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

Theorem tpres 6955
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 5560 . 2 (𝑇 ↾ (V ∖ {𝐴})) = (𝑇 ∩ ((V ∖ {𝐴}) × V))
2 elin 4166 . . . 4 (𝑥 ∈ (𝑇 ∩ ((V ∖ {𝐴}) × V)) ↔ (𝑥𝑇𝑥 ∈ ((V ∖ {𝐴}) × V)))
3 elxp 5571 . . . . . 6 (𝑥 ∈ ((V ∖ {𝐴}) × V) ↔ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))
43anbi2i 622 . . . . 5 ((𝑥𝑇𝑥 ∈ ((V ∖ {𝐴}) × V)) ↔ (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))
5 tpres.t . . . . . . . . 9 (𝜑𝑇 = {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
65eleq2d 2895 . . . . . . . 8 (𝜑 → (𝑥𝑇𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
7 vex 3495 . . . . . . . . . . . . 13 𝑥 ∈ V
87eltp 4618 . . . . . . . . . . . 12 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} ↔ (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
9 eldifsn 4711 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ (V ∖ {𝐴}) ↔ (𝑎 ∈ V ∧ 𝑎𝐴))
10 eqeq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 = ⟨𝐴, 𝐷⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩))
1110adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → (𝑥 = ⟨𝐴, 𝐷⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩))
12 vex 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
13 vex 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
1412, 13opth 5359 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐷))
15 eqneqall 3024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = 𝐴 → (𝑎𝐴 → (𝑏 = 𝐷 → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))))
1615com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎𝐴 → (𝑎 = 𝐴 → (𝑏 = 𝐷 → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))))
1716impd 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎𝐴 → ((𝑎 = 𝐴𝑏 = 𝐷) → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
1814, 17syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎𝐴 → (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩ → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
1918adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐷⟩ → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2011, 19sylbid 241 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → (𝑥 = ⟨𝐴, 𝐷⟩ → (𝜑 → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2120impd 411 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝐴𝑥 = ⟨𝑎, 𝑏⟩) → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2221ex 413 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2322adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ V ∧ 𝑎𝐴) → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
249, 23sylbi 218 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (V ∖ {𝐴}) → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2524adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V) → (𝑥 = ⟨𝑎, 𝑏⟩ → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
2625impcom 408 . . . . . . . . . . . . . . . . 17 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2726com12 32 . . . . . . . . . . . . . . . 16 ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2827exlimdvv 1926 . . . . . . . . . . . . . . 15 ((𝑥 = ⟨𝐴, 𝐷⟩ ∧ 𝜑) → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
2928ex 413 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝐴, 𝐷⟩ → (𝜑 → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))))
3029impd 411 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐴, 𝐷⟩ → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
31 orc 861 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝐵, 𝐸⟩ → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
3231a1d 25 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐵, 𝐸⟩ → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
33 olc 862 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝐶, 𝐹⟩ → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
3433a1d 25 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐶, 𝐹⟩ → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
3530, 32, 343jaoi 1419 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
368, 35sylbi 218 . . . . . . . . . . 11 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
377elpr 4580 . . . . . . . . . . 11 (𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} ↔ (𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
3836, 37syl6ibr 253 . . . . . . . . . 10 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → ((𝜑 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
3938expd 416 . . . . . . . . 9 (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (𝜑 → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})))
4039com12 32 . . . . . . . 8 (𝜑 → (𝑥 ∈ {⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})))
416, 40sylbid 241 . . . . . . 7 (𝜑 → (𝑥𝑇 → (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})))
4241impd 411 . . . . . 6 (𝜑 → ((𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) → 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
43 3mix2 1323 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐵, 𝐸⟩ → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
44 3mix3 1324 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐶, 𝐹⟩ → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
4543, 44jaoi 851 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
4645adantr 481 . . . . . . . . . . 11 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩))
476, 8syl6bb 288 . . . . . . . . . . . 12 (𝜑 → (𝑥𝑇 ↔ (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
4847adantl 482 . . . . . . . . . . 11 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → (𝑥𝑇 ↔ (𝑥 = ⟨𝐴, 𝐷⟩ ∨ 𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩)))
4946, 48mpbird 258 . . . . . . . . . 10 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → 𝑥𝑇)
50 tpres.b . . . . . . . . . . . . . . . 16 (𝜑𝐵𝑉)
5150elexd 3512 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ V)
52 tpres.1 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐴)
53 tpres.e . . . . . . . . . . . . . . . 16 (𝜑𝐸𝑉)
5453elexd 3512 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ V)
5551, 52, 54jca31 515 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V))
5655anim2i 616 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ 𝜑) → (𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)))
57 opeq12 4797 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝐵𝑏 = 𝐸) → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝐸⟩)
5857eqeq2d 2829 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐵𝑏 = 𝐸) → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝐸⟩))
59 eleq1 2897 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐵 → (𝑎 ∈ V ↔ 𝐵 ∈ V))
60 neeq1 3075 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐵 → (𝑎𝐴𝐵𝐴))
6159, 60anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝐵 → ((𝑎 ∈ V ∧ 𝑎𝐴) ↔ (𝐵 ∈ V ∧ 𝐵𝐴)))
62 eleq1 2897 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐸 → (𝑏 ∈ V ↔ 𝐸 ∈ V))
6361, 62bi2anan9 635 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐵𝑏 = 𝐸) → (((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V) ↔ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)))
6458, 63anbi12d 630 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝐵𝑏 = 𝐸) → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)) ↔ (𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V))))
6564spc2egv 3597 . . . . . . . . . . . . . . 15 ((𝐵𝑉𝐸𝑉) → ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
6650, 53, 65syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
6766adantl 482 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ 𝜑) → ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ ((𝐵 ∈ V ∧ 𝐵𝐴) ∧ 𝐸 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
6856, 67mpd 15 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐵, 𝐸⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
69 tpres.c . . . . . . . . . . . . . . . 16 (𝜑𝐶𝑉)
7069elexd 3512 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ V)
71 tpres.2 . . . . . . . . . . . . . . 15 (𝜑𝐶𝐴)
72 tpres.f . . . . . . . . . . . . . . . 16 (𝜑𝐹𝑉)
7372elexd 3512 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ V)
7470, 71, 73jca31 515 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V))
7574anim2i 616 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ 𝜑) → (𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)))
76 opeq12 4797 . . . . . . . . . . . . . . . . . 18 ((𝑎 = 𝐶𝑏 = 𝐹) → ⟨𝑎, 𝑏⟩ = ⟨𝐶, 𝐹⟩)
7776eqeq2d 2829 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐶𝑏 = 𝐹) → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐶, 𝐹⟩))
78 eleq1 2897 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐶 → (𝑎 ∈ V ↔ 𝐶 ∈ V))
79 neeq1 3075 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝐶 → (𝑎𝐴𝐶𝐴))
8078, 79anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝐶 → ((𝑎 ∈ V ∧ 𝑎𝐴) ↔ (𝐶 ∈ V ∧ 𝐶𝐴)))
81 eleq1 2897 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝐹 → (𝑏 ∈ V ↔ 𝐹 ∈ V))
8280, 81bi2anan9 635 . . . . . . . . . . . . . . . . 17 ((𝑎 = 𝐶𝑏 = 𝐹) → (((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V) ↔ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)))
8377, 82anbi12d 630 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝐶𝑏 = 𝐹) → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)) ↔ (𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V))))
8483spc2egv 3597 . . . . . . . . . . . . . . 15 ((𝐶𝑉𝐹𝑉) → ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
8569, 72, 84syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
8685adantl 482 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ 𝜑) → ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ ((𝐶 ∈ V ∧ 𝐶𝐴) ∧ 𝐹 ∈ V)) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))))
8775, 86mpd 15 . . . . . . . . . . . 12 ((𝑥 = ⟨𝐶, 𝐹⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
8868, 87jaoian 950 . . . . . . . . . . 11 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
899anbi1i 623 . . . . . . . . . . . . 13 ((𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V) ↔ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V))
9089anbi2i 622 . . . . . . . . . . . 12 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) ↔ (𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
91902exbii 1840 . . . . . . . . . . 11 (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)) ↔ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ((𝑎 ∈ V ∧ 𝑎𝐴) ∧ 𝑏 ∈ V)))
9288, 91sylibr 235 . . . . . . . . . 10 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))
9349, 92jca 512 . . . . . . . . 9 (((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) ∧ 𝜑) → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))))
9493ex 413 . . . . . . . 8 ((𝑥 = ⟨𝐵, 𝐸⟩ ∨ 𝑥 = ⟨𝐶, 𝐹⟩) → (𝜑 → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))))
9537, 94sylbi 218 . . . . . . 7 (𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (𝜑 → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))))
9695com12 32 . . . . . 6 (𝜑 → (𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩} → (𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V)))))
9742, 96impbid 213 . . . . 5 (𝜑 → ((𝑥𝑇 ∧ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ (V ∖ {𝐴}) ∧ 𝑏 ∈ V))) ↔ 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
984, 97syl5bb 284 . . . 4 (𝜑 → ((𝑥𝑇𝑥 ∈ ((V ∖ {𝐴}) × V)) ↔ 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
992, 98syl5bb 284 . . 3 (𝜑 → (𝑥 ∈ (𝑇 ∩ ((V ∖ {𝐴}) × V)) ↔ 𝑥 ∈ {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}))
10099eqrdv 2816 . 2 (𝜑 → (𝑇 ∩ ((V ∖ {𝐴}) × V)) = {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
1011, 100syl5eq 2865 1 (𝜑 → (𝑇 ↾ (V ∖ {𝐴})) = {⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3o 1078   = wceq 1528  wex 1771  wcel 2105  wne 3013  Vcvv 3492  cdif 3930  cin 3932  {csn 4557  {cpr 4559  {ctp 4561  cop 4563   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-opab 5120  df-xp 5554  df-res 5560
This theorem is referenced by:  estrres  17377
  Copyright terms: Public domain W3C validator