Metamath Proof Explorer

Theorem tpres

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)

Ref Expression
Hypotheses tpres.t ⊢ ( 𝜑 → 𝑇 = { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )
tpres.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
tpres.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
tpres.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
tpres.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
tpres.1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
tpres.2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
Assertion tpres ( 𝜑 → ( 𝑇 ↾ ( V ∖ { 𝐴 } ) ) = { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )

Proof

Step Hyp Ref Expression
1 tpres.t ⊢ ( 𝜑 → 𝑇 = { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )
2 tpres.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3 tpres.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 tpres.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
5 tpres.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6 tpres.1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
7 tpres.2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
8 df-res ⊢ ( 𝑇 ↾ ( V ∖ { 𝐴 } ) ) = ( 𝑇 ∩ ( ( V ∖ { 𝐴 } ) × V ) )
9 elin ⊢ ( 𝑥 ∈ ( 𝑇 ∩ ( ( V ∖ { 𝐴 } ) × V ) ) ↔ ( 𝑥 ∈ 𝑇 ∧ 𝑥 ∈ ( ( V ∖ { 𝐴 } ) × V ) ) )
10 elxp ⊢ ( 𝑥 ∈ ( ( V ∖ { 𝐴 } ) × V ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) )
11 10 anbi2i ⊢ ( ( 𝑥 ∈ 𝑇 ∧ 𝑥 ∈ ( ( V ∖ { 𝐴 } ) × V ) ) ↔ ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) )
12 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 ↔ 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
13 vex ⊢ 𝑥 ∈ V
14 13 eltp ⊢ ( 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ↔ ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
15 eldifsn ⊢ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ↔ ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) )
16 eqeq1 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ ) )
17 16 adantl ⊢ ( ( 𝑎 ≠ 𝐴 ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ ) )
18 vex ⊢ 𝑎 ∈ V
19 vex ⊢ 𝑏 ∈ V
20 18 19 opth ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ ↔ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐷 ) )
21 eqneqall ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ≠ 𝐴 → ( 𝑏 = 𝐷 → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) ) )
22 21 com12 ⊢ ( 𝑎 ≠ 𝐴 → ( 𝑎 = 𝐴 → ( 𝑏 = 𝐷 → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) ) )
23 22 impd ⊢ ( 𝑎 ≠ 𝐴 → ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐷 ) → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
24 20 23 biimtrid ⊢ ( 𝑎 ≠ 𝐴 → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
25 24 adantr ⊢ ( ( 𝑎 ≠ 𝐴 ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
26 17 25 sylbid ⊢ ( ( 𝑎 ≠ 𝐴 ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
27 26 impd ⊢ ( ( 𝑎 ≠ 𝐴 ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
28 27 ex ⊢ ( 𝑎 ≠ 𝐴 → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
29 28 adantl ⊢ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
30 15 29 sylbi ⊢ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
31 30 adantr ⊢ ( ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
32 31 impcom ⊢ ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
33 32 com12 ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
34 33 exlimdvv ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∧ 𝜑 ) → ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
35 34 ex ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ → ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
36 35 impd ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ → ( ( 𝜑 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
37 orc ⊢ ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
38 37 a1d ⊢ ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ → ( ( 𝜑 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
39 olc ⊢ ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
40 39 a1d ⊢ ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ → ( ( 𝜑 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
41 36 38 40 3jaoi ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) → ( ( 𝜑 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
42 14 41 sylbi ⊢ ( 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( ( 𝜑 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
43 13 elpr ⊢ ( 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ↔ ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
44 42 43 imbitrrdi ⊢ ( 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( ( 𝜑 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
45 44 expd ⊢ ( 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( 𝜑 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) ) )
46 45 com12 ⊢ ( 𝜑 → ( 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) ) )
47 12 46 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) → 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) ) )
48 47 impd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) → 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
49 3mix2 ⊢ ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
50 3mix3 ⊢ ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
51 49 50 jaoi ⊢ ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
52 51 adantr ⊢ ( ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
53 12 14 bitrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
54 53 adantl ⊢ ( ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ∧ 𝜑 ) → ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 = ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) )
55 52 54 mpbird ⊢ ( ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ∧ 𝜑 ) → 𝑥 ∈ 𝑇 )
56 2 elexd ⊢ ( 𝜑 → 𝐵 ∈ V )
57 4 elexd ⊢ ( 𝜑 → 𝐸 ∈ V )
58 56 6 57 jca31 ⊢ ( 𝜑 → ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) )
59 58 anim2i ⊢ ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) ) )
60 opeq12 ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐸 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐵 , 𝐸 ⟩ )
61 60 eqeq2d ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐸 ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ) )
62 eleq1 ⊢ ( 𝑎 = 𝐵 → ( 𝑎 ∈ V ↔ 𝐵 ∈ V ) )
63 neeq1 ⊢ ( 𝑎 = 𝐵 → ( 𝑎 ≠ 𝐴 ↔ 𝐵 ≠ 𝐴 ) )
64 62 63 anbi12d ⊢ ( 𝑎 = 𝐵 → ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ↔ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ) )
65 eleq1 ⊢ ( 𝑏 = 𝐸 → ( 𝑏 ∈ V ↔ 𝐸 ∈ V ) )
66 64 65 bi2anan9 ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐸 ) → ( ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ↔ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) ) )
67 61 66 anbi12d ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐸 ) → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ↔ ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) ) ) )
68 67 spc2egv ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ) )
69 2 4 68 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ) )
70 69 adantl ⊢ ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ 𝜑 ) → ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ 𝐸 ∈ V ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ) )
71 59 70 mpd ⊢ ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) )
72 3 elexd ⊢ ( 𝜑 → 𝐶 ∈ V )
73 5 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
74 72 7 73 jca31 ⊢ ( 𝜑 → ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) )
75 74 anim2i ⊢ ( ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ 𝜑 ) → ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) ) )
76 opeq12 ⊢ ( ( 𝑎 = 𝐶 ∧ 𝑏 = 𝐹 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐶 , 𝐹 ⟩ )
77 76 eqeq2d ⊢ ( ( 𝑎 = 𝐶 ∧ 𝑏 = 𝐹 ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) )
78 eleq1 ⊢ ( 𝑎 = 𝐶 → ( 𝑎 ∈ V ↔ 𝐶 ∈ V ) )
79 neeq1 ⊢ ( 𝑎 = 𝐶 → ( 𝑎 ≠ 𝐴 ↔ 𝐶 ≠ 𝐴 ) )
80 78 79 anbi12d ⊢ ( 𝑎 = 𝐶 → ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ↔ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) )
81 eleq1 ⊢ ( 𝑏 = 𝐹 → ( 𝑏 ∈ V ↔ 𝐹 ∈ V ) )
82 80 81 bi2anan9 ⊢ ( ( 𝑎 = 𝐶 ∧ 𝑏 = 𝐹 ) → ( ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ↔ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) ) )
83 77 82 anbi12d ⊢ ( ( 𝑎 = 𝐶 ∧ 𝑏 = 𝐹 ) → ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ↔ ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) ) ) )
84 83 spc2egv ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ) )
85 3 5 84 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ) )
86 85 adantl ⊢ ( ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ 𝜑 ) → ( ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ∧ 𝐹 ∈ V ) ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) ) )
87 75 86 mpd ⊢ ( ( 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) )
88 71 87 jaoian ⊢ ( ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) )
89 15 anbi1i ⊢ ( ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ↔ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) )
90 89 anbi2i ⊢ ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ↔ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) )
91 90 2exbii ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( 𝑎 ∈ V ∧ 𝑎 ≠ 𝐴 ) ∧ 𝑏 ∈ V ) ) )
92 88 91 sylibr ⊢ ( ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) )
93 55 92 jca ⊢ ( ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ∧ 𝜑 ) → ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) )
94 93 ex ⊢ ( ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) → ( 𝜑 → ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) ) )
95 43 94 sylbi ⊢ ( 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( 𝜑 → ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) ) )
96 95 com12 ⊢ ( 𝜑 → ( 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) ) )
97 48 96 impbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑇 ∧ ∃ 𝑎 ∃ 𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( V ∖ { 𝐴 } ) ∧ 𝑏 ∈ V ) ) ) ↔ 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
98 11 97 bitrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑇 ∧ 𝑥 ∈ ( ( V ∖ { 𝐴 } ) × V ) ) ↔ 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
99 9 98 bitrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑇 ∩ ( ( V ∖ { 𝐴 } ) × V ) ) ↔ 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
100 99 eqrdv ⊢ ( 𝜑 → ( 𝑇 ∩ ( ( V ∖ { 𝐴 } ) × V ) ) = { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )
101 8 100 eqtrid ⊢ ( 𝜑 → ( 𝑇 ↾ ( V ∖ { 𝐴 } ) ) = { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )