Metamath Proof Explorer

Theorem frxp3

Description: Give well-foundedness over a triple Cartesian product. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
frxp3.1 ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
frxp3.2 ⊢ ( 𝜑 → 𝑆 Fr 𝐵 )
frxp3.3 ⊢ ( 𝜑 → 𝑇 Fr 𝐶 )
Assertion frxp3 ( 𝜑 → 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 frxp3.1 ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
3 frxp3.2 ⊢ ( 𝜑 → 𝑆 Fr 𝐵 )
4 frxp3.3 ⊢ ( 𝜑 → 𝑇 Fr 𝐶 )
5 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → 𝑅 Fr 𝐴 )
6 dmss ⊢ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → dom 𝑠 ⊆ dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
7 6 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → dom 𝑠 ⊆ dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
8 dmxpss ⊢ dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) ⊆ ( 𝐴 × 𝐵 )
9 7 8 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → dom 𝑠 ⊆ ( 𝐴 × 𝐵 ) )
10 dmss ⊢ ( dom 𝑠 ⊆ ( 𝐴 × 𝐵 ) → dom dom 𝑠 ⊆ dom ( 𝐴 × 𝐵 ) )
11 9 10 syl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → dom dom 𝑠 ⊆ dom ( 𝐴 × 𝐵 ) )
12 dmxpss ⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴
13 11 12 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → dom dom 𝑠 ⊆ 𝐴 )
14 vex ⊢ 𝑠 ∈ V
15 14 dmex ⊢ dom 𝑠 ∈ V
16 15 dmex ⊢ dom dom 𝑠 ∈ V
17 16 a1i ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → dom dom 𝑠 ∈ V )
18 relxp ⊢ Rel ( ( 𝐴 × 𝐵 ) × 𝐶 )
19 relss ⊢ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( Rel ( ( 𝐴 × 𝐵 ) × 𝐶 ) → Rel 𝑠 ) )
20 18 19 mpi ⊢ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → Rel 𝑠 )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → Rel 𝑠 )
22 reldm0 ⊢ ( Rel 𝑠 → ( 𝑠 = ∅ ↔ dom 𝑠 = ∅ ) )
23 21 22 syl ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ( 𝑠 = ∅ ↔ dom 𝑠 = ∅ ) )
24 relxp ⊢ Rel ( 𝐴 × 𝐵 )
25 relss ⊢ ( dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) ⊆ ( 𝐴 × 𝐵 ) → ( Rel ( 𝐴 × 𝐵 ) → Rel dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) )
26 8 24 25 mp2 ⊢ Rel dom ( ( 𝐴 × 𝐵 ) × 𝐶 )
27 relss ⊢ ( dom 𝑠 ⊆ dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( Rel dom ( ( 𝐴 × 𝐵 ) × 𝐶 ) → Rel dom 𝑠 ) )
28 6 26 27 mpisyl ⊢ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → Rel dom 𝑠 )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → Rel dom 𝑠 )
30 reldm0 ⊢ ( Rel dom 𝑠 → ( dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅ ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ( dom 𝑠 = ∅ ↔ dom dom 𝑠 = ∅ ) )
32 23 31 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ( 𝑠 = ∅ ↔ dom dom 𝑠 = ∅ ) )
33 32 necon3bid ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ( 𝑠 ≠ ∅ ↔ dom dom 𝑠 ≠ ∅ ) )
34 33 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ∧ 𝑠 ≠ ∅ ) → dom dom 𝑠 ≠ ∅ )
35 34 anasss ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → dom dom 𝑠 ≠ ∅ )
36 5 13 17 35 frd ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ∃ 𝑎 ∈ dom dom 𝑠 ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 )
37 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → 𝑆 Fr 𝐵 )
38 imassrn ⊢ ( dom 𝑠 “ { 𝑎 } ) ⊆ ran dom 𝑠
39 rnss ⊢ ( dom 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran dom 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) )
40 9 39 syl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ran dom 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) )
41 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
42 40 41 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ran dom 𝑠 ⊆ 𝐵 )
43 38 42 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ( dom 𝑠 “ { 𝑎 } ) ⊆ 𝐵 )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → ( dom 𝑠 “ { 𝑎 } ) ⊆ 𝐵 )
45 15 imaex ⊢ ( dom 𝑠 “ { 𝑎 } ) ∈ V
46 45 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → ( dom 𝑠 “ { 𝑎 } ) ∈ V )
47 imadisj ⊢ ( ( dom 𝑠 “ { 𝑎 } ) = ∅ ↔ ( dom dom 𝑠 ∩ { 𝑎 } ) = ∅ )
48 disjsn ⊢ ( ( dom dom 𝑠 ∩ { 𝑎 } ) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠 )
49 47 48 bitri ⊢ ( ( dom 𝑠 “ { 𝑎 } ) = ∅ ↔ ¬ 𝑎 ∈ dom dom 𝑠 )
50 49 necon2abii ⊢ ( 𝑎 ∈ dom dom 𝑠 ↔ ( dom 𝑠 “ { 𝑎 } ) ≠ ∅ )
51 50 biimpi ⊢ ( 𝑎 ∈ dom dom 𝑠 → ( dom 𝑠 “ { 𝑎 } ) ≠ ∅ )
52 51 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → ( dom 𝑠 “ { 𝑎 } ) ≠ ∅ )
53 37 44 46 52 frd ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → ∃ 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 )
54 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → 𝑇 Fr 𝐶 )
55 imassrn ⊢ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ⊆ ran 𝑠
56 rnss ⊢ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ran 𝑠 ⊆ ran ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
57 56 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ran 𝑠 ⊆ ran ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
58 rnxpss ⊢ ran ( ( 𝐴 × 𝐵 ) × 𝐶 ) ⊆ 𝐶
59 57 58 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ran 𝑠 ⊆ 𝐶 )
60 55 59 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ⊆ 𝐶 )
61 60 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ⊆ 𝐶 )
62 14 imaex ⊢ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∈ V
63 62 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∈ V )
64 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) )
65 vex ⊢ 𝑎 ∈ V
66 vex ⊢ 𝑏 ∈ V
67 65 66 elimasn ⊢ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ dom 𝑠 )
68 64 67 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ dom 𝑠 )
69 imadisj ⊢ ( ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) = ∅ ↔ ( dom 𝑠 ∩ { ⟨ 𝑎 , 𝑏 ⟩ } ) = ∅ )
70 disjsn ⊢ ( ( dom 𝑠 ∩ { ⟨ 𝑎 , 𝑏 ⟩ } ) = ∅ ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ dom 𝑠 )
71 69 70 bitri ⊢ ( ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) = ∅ ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ dom 𝑠 )
72 71 necon2abii ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ dom 𝑠 ↔ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ≠ ∅ )
73 68 72 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ≠ ∅ )
74 54 61 63 73 frd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ∃ 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 )
75 df-ot ⊢ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩
76 simprl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
77 opex ⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
78 vex ⊢ 𝑐 ∈ V
79 77 78 elimasn ⊢ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ 𝑠 )
80 76 79 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ 𝑠 )
81 75 80 eqeltrid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ 𝑠 )
82 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
83 82 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
84 el2xpss ⊢ ( ( 𝑞 ∈ 𝑠 ∧ 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ )
85 84 ancoms ⊢ ( ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ 𝑠 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ )
86 83 85 sylan ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ )
87 df-ne ⊢ ( 𝑖 ≠ 𝑐 ↔ ¬ 𝑖 = 𝑐 )
88 87 con2bii ⊢ ( 𝑖 = 𝑐 ↔ ¬ 𝑖 ≠ 𝑐 )
89 88 biimpi ⊢ ( 𝑖 = 𝑐 → ¬ 𝑖 ≠ 𝑐 )
90 89 intnand ⊢ ( 𝑖 = 𝑐 → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) )
91 90 adantl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 = 𝑐 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) )
92 breq1 ⊢ ( 𝑓 = 𝑖 → ( 𝑓 𝑇 𝑐 ↔ 𝑖 𝑇 𝑐 ) )
93 92 notbid ⊢ ( 𝑓 = 𝑖 → ( ¬ 𝑓 𝑇 𝑐 ↔ ¬ 𝑖 𝑇 𝑐 ) )
94 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 )
95 94 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 )
96 df-ot ⊢ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑖 ⟩
97 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 )
98 96 97 eqeltrrid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑖 ⟩ ∈ 𝑠 )
99 vex ⊢ 𝑖 ∈ V
100 77 99 elimasn ⊢ ( 𝑖 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑖 ⟩ ∈ 𝑠 )
101 98 100 sylibr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → 𝑖 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) )
102 93 95 101 rspcdva ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ¬ 𝑖 𝑇 𝑐 )
103 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → 𝑖 ≠ 𝑐 )
104 103 neneqd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ¬ 𝑖 = 𝑐 )
105 ioran ⊢ ( ¬ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ↔ ( ¬ 𝑖 𝑇 𝑐 ∧ ¬ 𝑖 = 𝑐 ) )
106 102 104 105 sylanbrc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ¬ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) )
107 106 intn3an3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ¬ ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) )
108 107 intnanrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑖 ≠ 𝑐 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) )
109 91 108 pm2.61dane ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) )
110 oteq2 ⊢ ( ℎ = 𝑏 → ⟨ 𝑎 , ℎ , 𝑖 ⟩ = ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ )
111 110 eleq1d ⊢ ( ℎ = 𝑏 → ( ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ↔ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) )
112 111 anbi2d ⊢ ( ℎ = 𝑏 → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) ) )
113 neeq1 ⊢ ( ℎ = 𝑏 → ( ℎ ≠ 𝑏 ↔ 𝑏 ≠ 𝑏 ) )
114 113 orbi1d ⊢ ( ℎ = 𝑏 → ( ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ ( 𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
115 neirr ⊢ ¬ 𝑏 ≠ 𝑏
116 orel1 ⊢ ( ¬ 𝑏 ≠ 𝑏 → ( ( 𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) → 𝑖 ≠ 𝑐 ) )
117 115 116 ax-mp ⊢ ( ( 𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) → 𝑖 ≠ 𝑐 )
118 olc ⊢ ( 𝑖 ≠ 𝑐 → ( 𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) )
119 117 118 impbii ⊢ ( ( 𝑏 ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ 𝑖 ≠ 𝑐 )
120 114 119 bitrdi ⊢ ( ℎ = 𝑏 → ( ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ 𝑖 ≠ 𝑐 ) )
121 120 anbi2d ⊢ ( ℎ = 𝑏 → ( ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ↔ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) ) )
122 121 notbid ⊢ ( ℎ = 𝑏 → ( ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ↔ ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) ) )
123 112 122 imbi12d ⊢ ( ℎ = 𝑏 → ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) ↔ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ 𝑖 ≠ 𝑐 ) ) ) )
124 109 123 mpbiri ⊢ ( ℎ = 𝑏 → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) )
125 124 impcom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ = 𝑏 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
126 breq1 ⊢ ( 𝑒 = ℎ → ( 𝑒 𝑆 𝑏 ↔ ℎ 𝑆 𝑏 ) )
127 126 notbid ⊢ ( 𝑒 = ℎ → ( ¬ 𝑒 𝑆 𝑏 ↔ ¬ ℎ 𝑆 𝑏 ) )
128 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 )
129 128 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 )
130 df-ot ⊢ ⟨ 𝑎 , ℎ , 𝑖 ⟩ = ⟨ ⟨ 𝑎 , ℎ ⟩ , 𝑖 ⟩
131 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 )
132 130 131 eqeltrrid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ⟨ ⟨ 𝑎 , ℎ ⟩ , 𝑖 ⟩ ∈ 𝑠 )
133 opex ⊢ ⟨ 𝑎 , ℎ ⟩ ∈ V
134 133 99 opeldm ⊢ ( ⟨ ⟨ 𝑎 , ℎ ⟩ , 𝑖 ⟩ ∈ 𝑠 → ⟨ 𝑎 , ℎ ⟩ ∈ dom 𝑠 )
135 132 134 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ⟨ 𝑎 , ℎ ⟩ ∈ dom 𝑠 )
136 vex ⊢ ℎ ∈ V
137 65 136 elimasn ⊢ ( ℎ ∈ ( dom 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , ℎ ⟩ ∈ dom 𝑠 )
138 135 137 sylibr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ℎ ∈ ( dom 𝑠 “ { 𝑎 } ) )
139 127 129 138 rspcdva ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ¬ ℎ 𝑆 𝑏 )
140 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ℎ ≠ 𝑏 )
141 140 neneqd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ¬ ℎ = 𝑏 )
142 ioran ⊢ ( ¬ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ↔ ( ¬ ℎ 𝑆 𝑏 ∧ ¬ ℎ = 𝑏 ) )
143 139 141 142 sylanbrc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ¬ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) )
144 143 intn3an2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ¬ ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) )
145 144 intnanrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ ℎ ≠ 𝑏 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
146 125 145 pm2.61dane ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
147 oteq1 ⊢ ( 𝑔 = 𝑎 → ⟨ 𝑔 , ℎ , 𝑖 ⟩ = ⟨ 𝑎 , ℎ , 𝑖 ⟩ )
148 147 eleq1d ⊢ ( 𝑔 = 𝑎 → ( ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ↔ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) )
149 148 anbi2d ⊢ ( 𝑔 = 𝑎 → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ) )
150 neeq1 ⊢ ( 𝑔 = 𝑎 → ( 𝑔 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
151 biidd ⊢ ( 𝑔 = 𝑎 → ( ℎ ≠ 𝑏 ↔ ℎ ≠ 𝑏 ) )
152 biidd ⊢ ( 𝑔 = 𝑎 → ( 𝑖 ≠ 𝑐 ↔ 𝑖 ≠ 𝑐 ) )
153 150 151 152 3orbi123d ⊢ ( 𝑔 = 𝑎 → ( ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
154 3orass ⊢ ( ( 𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
155 neirr ⊢ ¬ 𝑎 ≠ 𝑎
156 orel1 ⊢ ( ¬ 𝑎 ≠ 𝑎 → ( ( 𝑎 ≠ 𝑎 ∨ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) → ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
157 155 156 ax-mp ⊢ ( ( 𝑎 ≠ 𝑎 ∨ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) → ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) )
158 olc ⊢ ( ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) → ( 𝑎 ≠ 𝑎 ∨ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
159 157 158 impbii ⊢ ( ( 𝑎 ≠ 𝑎 ∨ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ↔ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) )
160 154 159 bitri ⊢ ( ( 𝑎 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) )
161 153 160 bitrdi ⊢ ( 𝑔 = 𝑎 → ( ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ↔ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
162 161 anbi2d ⊢ ( 𝑔 = 𝑎 → ( ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ↔ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) )
163 162 notbid ⊢ ( 𝑔 = 𝑎 → ( ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ↔ ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) )
164 149 163 imbi12d ⊢ ( 𝑔 = 𝑎 → ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) ↔ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑎 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) ) )
165 146 164 mpbiri ⊢ ( 𝑔 = 𝑎 → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) )
166 165 impcom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 = 𝑎 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
167 breq1 ⊢ ( 𝑑 = 𝑔 → ( 𝑑 𝑅 𝑎 ↔ 𝑔 𝑅 𝑎 ) )
168 167 notbid ⊢ ( 𝑑 = 𝑔 → ( ¬ 𝑑 𝑅 𝑎 ↔ ¬ 𝑔 𝑅 𝑎 ) )
169 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 )
170 169 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 )
171 df-ot ⊢ ⟨ 𝑔 , ℎ , 𝑖 ⟩ = ⟨ ⟨ 𝑔 , ℎ ⟩ , 𝑖 ⟩
172 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 )
173 171 172 eqeltrrid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ⟨ ⟨ 𝑔 , ℎ ⟩ , 𝑖 ⟩ ∈ 𝑠 )
174 opex ⊢ ⟨ 𝑔 , ℎ ⟩ ∈ V
175 174 99 opeldm ⊢ ( ⟨ ⟨ 𝑔 , ℎ ⟩ , 𝑖 ⟩ ∈ 𝑠 → ⟨ 𝑔 , ℎ ⟩ ∈ dom 𝑠 )
176 vex ⊢ 𝑔 ∈ V
177 176 136 opeldm ⊢ ( ⟨ 𝑔 , ℎ ⟩ ∈ dom 𝑠 → 𝑔 ∈ dom dom 𝑠 )
178 173 175 177 3syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → 𝑔 ∈ dom dom 𝑠 )
179 168 170 178 rspcdva ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ¬ 𝑔 𝑅 𝑎 )
180 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → 𝑔 ≠ 𝑎 )
181 180 neneqd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ¬ 𝑔 = 𝑎 )
182 ioran ⊢ ( ¬ ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ↔ ( ¬ 𝑔 𝑅 𝑎 ∧ ¬ 𝑔 = 𝑎 ) )
183 179 181 182 sylanbrc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ¬ ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) )
184 183 intn3an1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ¬ ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) )
185 184 intnanrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ∧ 𝑔 ≠ 𝑎 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
186 166 185 pm2.61dane ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) )
187 186 intn3an3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) )
188 eleq1 ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( 𝑞 ∈ 𝑠 ↔ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) )
189 188 anbi2d ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) ) )
190 breq1 ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ⟨ 𝑔 , ℎ , 𝑖 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
191 1 xpord3lem ⊢ ( ⟨ 𝑔 , ℎ , 𝑖 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) )
192 190 191 bitrdi ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) ) )
193 192 notbid ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ¬ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) ) )
194 189 193 imbi12d ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ ⟨ 𝑔 , ℎ , 𝑖 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑎 ∨ 𝑔 = 𝑎 ) ∧ ( ℎ 𝑆 𝑏 ∨ ℎ = 𝑏 ) ∧ ( 𝑖 𝑇 𝑐 ∨ 𝑖 = 𝑐 ) ) ∧ ( 𝑔 ≠ 𝑎 ∨ ℎ ≠ 𝑏 ∨ 𝑖 ≠ 𝑐 ) ) ) ) ) )
195 187 194 mpbiri ⊢ ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
196 195 com12 ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
197 196 exlimdv ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( ∃ 𝑖 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
198 197 exlimdvv ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( ∃ 𝑔 ∃ ℎ ∃ 𝑖 𝑞 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ → ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
199 86 198 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ )
200 199 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ )
201 breq2 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 𝑞 𝑈 𝑝 ↔ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
202 201 notbid ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ¬ 𝑞 𝑈 𝑝 ↔ ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
203 202 ralbidv ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 ↔ ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
204 203 rspcev ⊢ ( ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ 𝑠 ∧ ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 )
205 81 200 204 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ∧ ∀ 𝑓 ∈ ( 𝑠 “ { ⟨ 𝑎 , 𝑏 ⟩ } ) ¬ 𝑓 𝑇 𝑐 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 )
206 74 205 rexlimddv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) ∧ ( 𝑏 ∈ ( dom 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑒 ∈ ( dom 𝑠 “ { 𝑎 } ) ¬ 𝑒 𝑆 𝑏 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 )
207 53 206 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom dom 𝑠 ∧ ∀ 𝑑 ∈ dom dom 𝑠 ¬ 𝑑 𝑅 𝑎 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 )
208 36 207 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 )
209 208 ex ⊢ ( 𝜑 → ( ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 ) )
210 209 alrimiv ⊢ ( 𝜑 → ∀ 𝑠 ( ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 ) )
211 df-fr ⊢ ( 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∀ 𝑠 ( ( 𝑠 ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑈 𝑝 ) )
212 210 211 sylibr ⊢ ( 𝜑 → 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) )