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