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 syl5bi ( 𝑎𝐴 → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ → ( 𝜑 → ( 𝑥 = ⟨ 𝐵 , 𝐸 ⟩ ∨ 𝑥 = ⟨ 𝐶 , 𝐹 ⟩ ) ) ) )
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 syl6ibr ( 𝑥 ∈ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( ( 𝜑 ∧ ∃ 𝑎𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ ( 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 syl5bb ( 𝜑 → ( ( 𝑥𝑇𝑥 ∈ ( ( V ∖ { 𝐴 } ) × V ) ) ↔ 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
99 9 98 syl5bb ( 𝜑 → ( 𝑥 ∈ ( 𝑇 ∩ ( ( V ∖ { 𝐴 } ) × V ) ) ↔ 𝑥 ∈ { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ) )
100 99 eqrdv ( 𝜑 → ( 𝑇 ∩ ( ( V ∖ { 𝐴 } ) × V ) ) = { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )
101 8 100 eqtrid ( 𝜑 → ( 𝑇 ↾ ( V ∖ { 𝐴 } ) ) = { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )