Metamath Proof Explorer

Theorem frxp3

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