ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  brtpos2 Structured version   GIF version

Theorem brtpos2 5784
Description: Value of the transposition at a pair A, B. (Contributed by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
brtpos2 (B 𝑉 → (Atpos 𝐹B ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B)))

Proof of Theorem brtpos2
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reltpos 5783 . . . 4 Rel tpos 𝐹
21brrelexi 4307 . . 3 (Atpos 𝐹BA V)
32a1i 9 . 2 (B 𝑉 → (Atpos 𝐹BA V))
4 elex 2539 . . . 4 (A (dom 𝐹 ∪ {∅}) → A V)
54adantr 261 . . 3 ((A (dom 𝐹 ∪ {∅}) {A}𝐹B) → A V)
65a1i 9 . 2 (B 𝑉 → ((A (dom 𝐹 ∪ {∅}) {A}𝐹B) → A V))
7 df-tpos 5778 . . . . . 6 tpos 𝐹 = (𝐹 ∘ (x (dom 𝐹 ∪ {∅}) ↦ {x}))
87breqi 3740 . . . . 5 (Atpos 𝐹BA(𝐹 ∘ (x (dom 𝐹 ∪ {∅}) ↦ {x}))B)
9 brcog 4425 . . . . 5 ((A V B 𝑉) → (A(𝐹 ∘ (x (dom 𝐹 ∪ {∅}) ↦ {x}))By(A(x (dom 𝐹 ∪ {∅}) ↦ {x})y y𝐹B)))
108, 9syl5bb 181 . . . 4 ((A V B 𝑉) → (Atpos 𝐹By(A(x (dom 𝐹 ∪ {∅}) ↦ {x})y y𝐹B)))
11 funmpt 4860 . . . . . . . . . . 11 Fun (x (dom 𝐹 ∪ {∅}) ↦ {x})
12 funbrfv2b 5139 . . . . . . . . . . 11 (Fun (x (dom 𝐹 ∪ {∅}) ↦ {x}) → (A(x (dom 𝐹 ∪ {∅}) ↦ {x})y ↔ (A dom (x (dom 𝐹 ∪ {∅}) ↦ {x}) ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = y)))
1311, 12ax-mp 7 . . . . . . . . . 10 (A(x (dom 𝐹 ∪ {∅}) ↦ {x})y ↔ (A dom (x (dom 𝐹 ∪ {∅}) ↦ {x}) ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = y))
14 vex 2534 . . . . . . . . . . . . . . . . 17 x V
15 snexg 3906 . . . . . . . . . . . . . . . . 17 (x V → {x} V)
1614, 15ax-mp 7 . . . . . . . . . . . . . . . 16 {x} V
1716cnvex 4779 . . . . . . . . . . . . . . 15 {x} V
1817uniex 4120 . . . . . . . . . . . . . 14 {x} V
19 eqid 2018 . . . . . . . . . . . . . 14 (x (dom 𝐹 ∪ {∅}) ↦ {x}) = (x (dom 𝐹 ∪ {∅}) ↦ {x})
2018, 19dmmpti 4950 . . . . . . . . . . . . 13 dom (x (dom 𝐹 ∪ {∅}) ↦ {x}) = (dom 𝐹 ∪ {∅})
2120eleq2i 2082 . . . . . . . . . . . 12 (A dom (x (dom 𝐹 ∪ {∅}) ↦ {x}) ↔ A (dom 𝐹 ∪ {∅}))
22 eqcom 2020 . . . . . . . . . . . 12 (((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = yy = ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A))
2321, 22anbi12i 436 . . . . . . . . . . 11 ((A dom (x (dom 𝐹 ∪ {∅}) ↦ {x}) ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = y) ↔ (A (dom 𝐹 ∪ {∅}) y = ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A)))
24 snexg 3906 . . . . . . . . . . . . . . . 16 (A (dom 𝐹 ∪ {∅}) → {A} V)
25 cnvexg 4778 . . . . . . . . . . . . . . . 16 ({A} V → {A} V)
2624, 25syl 14 . . . . . . . . . . . . . . 15 (A (dom 𝐹 ∪ {∅}) → {A} V)
27 uniexg 4121 . . . . . . . . . . . . . . 15 ({A} V → {A} V)
2826, 27syl 14 . . . . . . . . . . . . . 14 (A (dom 𝐹 ∪ {∅}) → {A} V)
29 sneq 3357 . . . . . . . . . . . . . . . . 17 (x = A → {x} = {A})
3029cnveqd 4434 . . . . . . . . . . . . . . . 16 (x = A{x} = {A})
3130unieqd 3561 . . . . . . . . . . . . . . 15 (x = A {x} = {A})
3231, 19fvmptg 5169 . . . . . . . . . . . . . 14 ((A (dom 𝐹 ∪ {∅}) {A} V) → ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = {A})
3328, 32mpdan 400 . . . . . . . . . . . . 13 (A (dom 𝐹 ∪ {∅}) → ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = {A})
3433eqeq2d 2029 . . . . . . . . . . . 12 (A (dom 𝐹 ∪ {∅}) → (y = ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) ↔ y = {A}))
3534pm5.32i 430 . . . . . . . . . . 11 ((A (dom 𝐹 ∪ {∅}) y = ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A)) ↔ (A (dom 𝐹 ∪ {∅}) y = {A}))
3623, 35bitri 173 . . . . . . . . . 10 ((A dom (x (dom 𝐹 ∪ {∅}) ↦ {x}) ((x (dom 𝐹 ∪ {∅}) ↦ {x})‘A) = y) ↔ (A (dom 𝐹 ∪ {∅}) y = {A}))
3713, 36bitri 173 . . . . . . . . 9 (A(x (dom 𝐹 ∪ {∅}) ↦ {x})y ↔ (A (dom 𝐹 ∪ {∅}) y = {A}))
38 ancom 253 . . . . . . . . 9 ((A (dom 𝐹 ∪ {∅}) y = {A}) ↔ (y = {A} A (dom 𝐹 ∪ {∅})))
3937, 38bitri 173 . . . . . . . 8 (A(x (dom 𝐹 ∪ {∅}) ↦ {x})y ↔ (y = {A} A (dom 𝐹 ∪ {∅})))
4039anbi1i 434 . . . . . . 7 ((A(x (dom 𝐹 ∪ {∅}) ↦ {x})y y𝐹B) ↔ ((y = {A} A (dom 𝐹 ∪ {∅})) y𝐹B))
41 anass 383 . . . . . . 7 (((y = {A} A (dom 𝐹 ∪ {∅})) y𝐹B) ↔ (y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)))
4240, 41bitri 173 . . . . . 6 ((A(x (dom 𝐹 ∪ {∅}) ↦ {x})y y𝐹B) ↔ (y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)))
4342exbii 1474 . . . . 5 (y(A(x (dom 𝐹 ∪ {∅}) ↦ {x})y y𝐹B) ↔ y(y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)))
44 exsimpr 1487 . . . . . . 7 (y(y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)) → y(A (dom 𝐹 ∪ {∅}) y𝐹B))
45 exsimpl 1486 . . . . . . . 8 (y(A (dom 𝐹 ∪ {∅}) y𝐹B) → y A (dom 𝐹 ∪ {∅}))
46 19.9v 1729 . . . . . . . 8 (y A (dom 𝐹 ∪ {∅}) ↔ A (dom 𝐹 ∪ {∅}))
4745, 46sylib 127 . . . . . . 7 (y(A (dom 𝐹 ∪ {∅}) y𝐹B) → A (dom 𝐹 ∪ {∅}))
4844, 47syl 14 . . . . . 6 (y(y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)) → A (dom 𝐹 ∪ {∅}))
49 ax-ia1 99 . . . . . 6 ((A (dom 𝐹 ∪ {∅}) {A}𝐹B) → A (dom 𝐹 ∪ {∅}))
50 breq1 3737 . . . . . . . . 9 (y = {A} → (y𝐹B {A}𝐹B))
5150anbi2d 440 . . . . . . . 8 (y = {A} → ((A (dom 𝐹 ∪ {∅}) y𝐹B) ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B)))
5251ceqsexgv 2646 . . . . . . 7 ( {A} V → (y(y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)) ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B)))
5328, 52syl 14 . . . . . 6 (A (dom 𝐹 ∪ {∅}) → (y(y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)) ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B)))
5448, 49, 53pm5.21nii 607 . . . . 5 (y(y = {A} (A (dom 𝐹 ∪ {∅}) y𝐹B)) ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B))
5543, 54bitri 173 . . . 4 (y(A(x (dom 𝐹 ∪ {∅}) ↦ {x})y y𝐹B) ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B))
5610, 55syl6bb 185 . . 3 ((A V B 𝑉) → (Atpos 𝐹B ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B)))
5756expcom 109 . 2 (B 𝑉 → (A V → (Atpos 𝐹B ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B))))
583, 6, 57pm5.21ndd 608 1 (B 𝑉 → (Atpos 𝐹B ↔ (A (dom 𝐹 ∪ {∅}) {A}𝐹B)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1226  wex 1358   wcel 1370  Vcvv 2531  cun 2888  c0 3197  {csn 3346   cuni 3550   class class class wbr 3734  cmpt 3788  ccnv 4267  dom cdm 4268  ccom 4272  Fun wfun 4819  cfv 4825  tpos ctpos 5777
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-un 4116
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-mpt 3790  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-fv 4833  df-tpos 5778
This theorem is referenced by:  brtpos0  5785  reldmtpos  5786  brtposg  5787  dftpos4  5796  tpostpos  5797
  Copyright terms: Public domain W3C validator