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

Theorem cnvf1olem 5845
 Description: Lemma for cnvf1o 5846. (Contributed by Mario Carneiro, 27-Apr-2014.)
Assertion
Ref Expression
cnvf1olem ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → (𝐶𝐴𝐵 = {𝐶}))

Proof of Theorem cnvf1olem
StepHypRef Expression
1 simprr 484 . . . 4 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → 𝐶 = {𝐵})
2 1st2nd 5807 . . . . . . . 8 ((Rel 𝐴𝐵𝐴) → 𝐵 = ⟨(1st𝐵), (2nd𝐵)⟩)
32adantrr 448 . . . . . . 7 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → 𝐵 = ⟨(1st𝐵), (2nd𝐵)⟩)
43sneqd 3388 . . . . . 6 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {𝐵} = {⟨(1st𝐵), (2nd𝐵)⟩})
54cnveqd 4511 . . . . 5 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {𝐵} = {⟨(1st𝐵), (2nd𝐵)⟩})
65unieqd 3591 . . . 4 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {𝐵} = {⟨(1st𝐵), (2nd𝐵)⟩})
7 1stexg 5794 . . . . . 6 (𝐵𝐴 → (1st𝐵) ∈ V)
8 2ndexg 5795 . . . . . 6 (𝐵𝐴 → (2nd𝐵) ∈ V)
9 opswapg 4807 . . . . . 6 (((1st𝐵) ∈ V ∧ (2nd𝐵) ∈ V) → {⟨(1st𝐵), (2nd𝐵)⟩} = ⟨(2nd𝐵), (1st𝐵)⟩)
107, 8, 9syl2anc 391 . . . . 5 (𝐵𝐴 {⟨(1st𝐵), (2nd𝐵)⟩} = ⟨(2nd𝐵), (1st𝐵)⟩)
1110ad2antrl 459 . . . 4 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {⟨(1st𝐵), (2nd𝐵)⟩} = ⟨(2nd𝐵), (1st𝐵)⟩)
121, 6, 113eqtrd 2076 . . 3 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → 𝐶 = ⟨(2nd𝐵), (1st𝐵)⟩)
13 simprl 483 . . . . 5 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → 𝐵𝐴)
143, 13eqeltrrd 2115 . . . 4 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ 𝐴)
15 opelcnvg 4515 . . . . . 6 (((2nd𝐵) ∈ V ∧ (1st𝐵) ∈ V) → (⟨(2nd𝐵), (1st𝐵)⟩ ∈ 𝐴 ↔ ⟨(1st𝐵), (2nd𝐵)⟩ ∈ 𝐴))
168, 7, 15syl2anc 391 . . . . 5 (𝐵𝐴 → (⟨(2nd𝐵), (1st𝐵)⟩ ∈ 𝐴 ↔ ⟨(1st𝐵), (2nd𝐵)⟩ ∈ 𝐴))
1716ad2antrl 459 . . . 4 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → (⟨(2nd𝐵), (1st𝐵)⟩ ∈ 𝐴 ↔ ⟨(1st𝐵), (2nd𝐵)⟩ ∈ 𝐴))
1814, 17mpbird 156 . . 3 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → ⟨(2nd𝐵), (1st𝐵)⟩ ∈ 𝐴)
1912, 18eqeltrd 2114 . 2 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → 𝐶𝐴)
20 opswapg 4807 . . . . . 6 (((2nd𝐵) ∈ V ∧ (1st𝐵) ∈ V) → {⟨(2nd𝐵), (1st𝐵)⟩} = ⟨(1st𝐵), (2nd𝐵)⟩)
218, 7, 20syl2anc 391 . . . . 5 (𝐵𝐴 {⟨(2nd𝐵), (1st𝐵)⟩} = ⟨(1st𝐵), (2nd𝐵)⟩)
2221eqcomd 2045 . . . 4 (𝐵𝐴 → ⟨(1st𝐵), (2nd𝐵)⟩ = {⟨(2nd𝐵), (1st𝐵)⟩})
2322ad2antrl 459 . . 3 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → ⟨(1st𝐵), (2nd𝐵)⟩ = {⟨(2nd𝐵), (1st𝐵)⟩})
2412sneqd 3388 . . . . 5 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {𝐶} = {⟨(2nd𝐵), (1st𝐵)⟩})
2524cnveqd 4511 . . . 4 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {𝐶} = {⟨(2nd𝐵), (1st𝐵)⟩})
2625unieqd 3591 . . 3 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → {𝐶} = {⟨(2nd𝐵), (1st𝐵)⟩})
2723, 3, 263eqtr4d 2082 . 2 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → 𝐵 = {𝐶})
2819, 27jca 290 1 ((Rel 𝐴 ∧ (𝐵𝐴𝐶 = {𝐵})) → (𝐶𝐴𝐵 = {𝐶}))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  Vcvv 2557  {csn 3375  ⟨cop 3378  ∪ cuni 3580  ◡ccnv 4344  Rel wrel 4350  ‘cfv 4902  1st c1st 5765  2nd c2nd 5766 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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-un 4170 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-sbc 2765  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-mpt 3820  df-id 4030  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-fo 4908  df-fv 4910  df-1st 5767  df-2nd 5768 This theorem is referenced by:  cnvf1o  5846
 Copyright terms: Public domain W3C validator