MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tpres Structured version   Visualization version   GIF version

Theorem tpres 7016
Description: An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020.)
Hypotheses
Ref Expression
tpres.t (𝜑𝑇 = {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
tpres.b (𝜑𝐵𝑉)
tpres.c (𝜑𝐶𝑉)
tpres.e (𝜑𝐸𝑉)
tpres.f (𝜑𝐹𝑉)
tpres.1 (𝜑𝐵𝐴)
tpres.2 (𝜑𝐶𝐴)
Assertion
Ref Expression
tpres (𝜑 → (𝑇 ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})

Proof of Theorem tpres
Dummy variables 𝑎 𝑏 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-res 5563 . 2 (𝑇 ↾ (V ∖ {𝐴})) = (𝑇 ∩ ((V ∖ {𝐴}) × V))
2 elin 3882 . . . 4 (𝑥 ∈ (𝑇 ∩ ((V ∖ {𝐴}) × V)) ↔ (𝑥𝑇𝑥 ∈ ((V ∖ {𝐴}) × V)))
3 elxp 5574 . . . . . 6 (𝑥 ∈ ((V ∖ {𝐴}) × V) ↔ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))
43anbi2i 626 . . . . 5 ((𝑥𝑇𝑥 ∈ ((V ∖ {𝐴}) × V)) ↔ (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))
5 tpres.t . . . . . . . . 9 (𝜑𝑇 = {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
65eleq2d 2823 . . . . . . . 8 (𝜑 → (𝑥𝑇𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
7 vex 3412 . . . . . . . . . . . . 13 𝑥 ∈ V
87eltp 4604 . . . . . . . . . . . 12 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} ↔ (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
9 eldifsn 4700 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (V ∖ {𝐴}) ↔ (𝑎 ∈ V ∧ 𝑎𝐴))
10 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 = ⟨𝐴, 𝐷⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩))
1110adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → (𝑥 = ⟨𝐴, 𝐷⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩))
12 vex 3412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
13 vex 3412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
1412, 13opth 5360 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐷))
15 eqneqall 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = 𝐴 → (𝑎𝐴 → (𝑏 = 𝐷 → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))))
1615com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎𝐴 → (𝑎 = 𝐴 → (𝑏 = 𝐷 → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))))
1716impd 414 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎𝐴 → ((𝑎 = 𝐴𝑏 = 𝐷) → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
1814, 17syl5bi 245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎𝐴 → (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩ → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
1918adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩ → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2011, 19sylbid 243 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → (𝑥 = ⟨𝐴, 𝐷⟩ → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2120impd 414 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2221ex 416 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2322adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎𝐴) → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
249, 23sylbi 220 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (V ∖ {𝐴}) → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2524adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V) → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2625impcom 411 . . . . . . . . . . . . . . . . 17 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2726com12 32 . . . . . . . . . . . . . . . 16 ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2827exlimdvv 1942 . . . . . . . . . . . . . . 15 ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2928ex 416 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝐴, 𝐷⟩ → (𝜑 → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
3029impd 414 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐴, 𝐷⟩ → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
31 orc 867 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝐵, 𝐸⟩ → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
3231a1d 25 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐵, 𝐸⟩ → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
33 olc 868 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝐶, 𝐹⟩ → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
3433a1d 25 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐶, 𝐹⟩ → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
3530, 32, 343jaoi 1429 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
368, 35sylbi 220 . . . . . . . . . . 11 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
377elpr 4564 . . . . . . . . . . 11 (𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} ↔ (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
3836, 37syl6ibr 255 . . . . . . . . . 10 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
3938expd 419 . . . . . . . . 9 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (𝜑 → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})))
4039com12 32 . . . . . . . 8 (𝜑 → (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})))
416, 40sylbid 243 . . . . . . 7 (𝜑 → (𝑥𝑇 → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})))
4241impd 414 . . . . . 6 (𝜑 → ((𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
43 3mix2 1333 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐵, 𝐸⟩ → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
44 3mix3 1334 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐶, 𝐹⟩ → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
4543, 44jaoi 857 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
4645adantr 484 . . . . . . . . . . 11 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
476, 8bitrdi 290 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑇 ↔ (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
4847adantl 485 . . . . . . . . . . 11 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → (𝑥𝑇 ↔ (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
4946, 48mpbird 260 . . . . . . . . . 10 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → 𝑥𝑇)
50 tpres.b . . . . . . . . . . . . . . . 16 (𝜑𝐵𝑉)
5150elexd 3428 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ V)
52 tpres.1 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐴)
53 tpres.e . . . . . . . . . . . . . . . 16 (𝜑𝐸𝑉)
5453elexd 3428 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ V)
5551, 52, 54jca31 518 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V))
5655anim2i 620 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)))
57 opeq12 4786 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝐵𝑏 = 𝐸) → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝐸⟩)
5857eqeq2d 2748 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐵𝑏 = 𝐸) → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝐸⟩))
59 eleq1 2825 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐵 → (𝑎 ∈ V ↔ 𝐵 ∈ V))
60 neeq1 3003 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐵 → (𝑎𝐴𝐵𝐴))
6159, 60anbi12d 634 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝐵 → ((𝑎 ∈ V ∧ 𝑎𝐴) ↔ (𝐵 ∈ V ∧ 𝐵𝐴)))
62 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐸 → (𝑏 ∈ V ↔ 𝐸 ∈ V))
6361, 62bi2anan9 639 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐵𝑏 = 𝐸) → (((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V) ↔ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)))
6458, 63anbi12d 634 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝐵𝑏 = 𝐸) → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)) ↔ (𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V))))
6564spc2egv 3514 . . . . . . . . . . . . . . 15 ((𝐵𝑉𝐸𝑉) → ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
6650, 53, 65syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
6766adantl 485 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ 𝜑) → ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
6856, 67mpd 15 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
69 tpres.c . . . . . . . . . . . . . . . 16 (𝜑𝐶𝑉)
7069elexd 3428 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ V)
71 tpres.2 . . . . . . . . . . . . . . 15 (𝜑𝐶𝐴)
72 tpres.f . . . . . . . . . . . . . . . 16 (𝜑𝐹𝑉)
7372elexd 3428 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ V)
7470, 71, 73jca31 518 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V))
7574anim2i 620 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ 𝜑) → (𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)))
76 opeq12 4786 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝐶𝑏 = 𝐹) → ⟨𝑎, 𝑏⟩ = ⟨𝐶, 𝐹⟩)
7776eqeq2d 2748 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐶𝑏 = 𝐹) → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐶, 𝐹⟩))
78 eleq1 2825 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐶 → (𝑎 ∈ V ↔ 𝐶 ∈ V))
79 neeq1 3003 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐶 → (𝑎𝐴𝐶𝐴))
8078, 79anbi12d 634 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝐶 → ((𝑎 ∈ V ∧ 𝑎𝐴) ↔ (𝐶 ∈ V ∧ 𝐶𝐴)))
81 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐹 → (𝑏 ∈ V ↔ 𝐹 ∈ V))
8280, 81bi2anan9 639 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐶𝑏 = 𝐹) → (((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V) ↔ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)))
8377, 82anbi12d 634 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝐶𝑏 = 𝐹) → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)) ↔ (𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V))))
8483spc2egv 3514 . . . . . . . . . . . . . . 15 ((𝐶𝑉𝐹𝑉) → ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
8569, 72, 84syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
8685adantl 485 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ 𝜑) → ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
8775, 86mpd 15 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
8868, 87jaoian 957 . . . . . . . . . . 11 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
899anbi1i 627 . . . . . . . . . . . . 13 ((𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V) ↔ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))
9089anbi2i 626 . . . . . . . . . . . 12 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) ↔ (𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
91902exbii 1856 . . . . . . . . . . 11 (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) ↔ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
9288, 91sylibr 237 . . . . . . . . . 10 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))
9349, 92jca 515 . . . . . . . . 9 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))
9493ex 416 . . . . . . . 8 ((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) → (𝜑 → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))))
9537, 94sylbi 220 . . . . . . 7 (𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (𝜑 → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))))
9695com12 32 . . . . . 6 (𝜑 → (𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))))
9742, 96impbid 215 . . . . 5 (𝜑 → ((𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) ↔ 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
984, 97syl5bb 286 . . . 4 (𝜑 → ((𝑥𝑇𝑥 ∈ ((V ∖ {𝐴}) × V)) ↔ 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
992, 98syl5bb 286 . . 3 (𝜑 → (𝑥 ∈ (𝑇 ∩ ((V ∖ {𝐴}) × V)) ↔ 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
10099eqrdv 2735 . 2 (𝜑 → (𝑇 ∩ ((V ∖ {𝐴}) × V)) = {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
1011, 100eqtrid 2789 1 (𝜑 → (𝑇 ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3o 1088   = wceq 1543  wex 1787  wcel 2110  wne 2940  Vcvv 3408  cdif 3863  cin 3865  {csn 4541  {cpr 4543  {ctp 4545  cop 4547   × cxp 5549  cres 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-opab 5116  df-xp 5557  df-res 5563
This theorem is referenced by:  estrres  17646  symgvalstruct  18789
  Copyright terms: Public domain W3C validator