Metamath Proof Explorer

Theorem frxp2

Description: Another way of giving a well-founded order to a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 xpord2.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 frxp2.1 ⊢ ( 𝜑 → 𝑅 Fr 𝐴 )
3 frxp2.2 ⊢ ( 𝜑 → 𝑆 Fr 𝐵 )
4 dmss ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → dom 𝑠 ⊆ dom ( 𝐴 × 𝐵 ) )
5 4 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → dom 𝑠 ⊆ dom ( 𝐴 × 𝐵 ) )
6 dmxpss ⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴
7 5 6 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → dom 𝑠 ⊆ 𝐴 )
8 simprr ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → 𝑠 ≠ ∅ )
9 relxp ⊢ Rel ( 𝐴 × 𝐵 )
10 relss ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( Rel ( 𝐴 × 𝐵 ) → Rel 𝑠 ) )
11 9 10 mpi ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → Rel 𝑠 )
12 11 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → Rel 𝑠 )
13 reldm0 ⊢ ( Rel 𝑠 → ( 𝑠 = ∅ ↔ dom 𝑠 = ∅ ) )
14 12 13 syl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ( 𝑠 = ∅ ↔ dom 𝑠 = ∅ ) )
15 14 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ( 𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅ ) )
16 8 15 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → dom 𝑠 ≠ ∅ )
17 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → 𝑅 Fr 𝐴 )
18 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑐 ( ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑐 ¬ 𝑏 𝑅 𝑎 ) )
19 17 18 sylib ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ∀ 𝑐 ( ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑐 ¬ 𝑏 𝑅 𝑎 ) )
20 vex ⊢ 𝑠 ∈ V
21 20 dmex ⊢ dom 𝑠 ∈ V
22 sseq1 ⊢ ( 𝑐 = dom 𝑠 → ( 𝑐 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴 ) )
23 neeq1 ⊢ ( 𝑐 = dom 𝑠 → ( 𝑐 ≠ ∅ ↔ dom 𝑠 ≠ ∅ ) )
24 22 23 anbi12d ⊢ ( 𝑐 = dom 𝑠 → ( ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅ ) ↔ ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) ) )
25 raleq ⊢ ( 𝑐 = dom 𝑠 → ( ∀ 𝑏 ∈ 𝑐 ¬ 𝑏 𝑅 𝑎 ↔ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) )
26 25 rexeqbi1dv ⊢ ( 𝑐 = dom 𝑠 → ( ∃ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑐 ¬ 𝑏 𝑅 𝑎 ↔ ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) )
27 24 26 imbi12d ⊢ ( 𝑐 = dom 𝑠 → ( ( ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑐 ¬ 𝑏 𝑅 𝑎 ) ↔ ( ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) )
28 21 27 spcv ⊢ ( ∀ 𝑐 ( ( 𝑐 ⊆ 𝐴 ∧ 𝑐 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑐 ∀ 𝑏 ∈ 𝑐 ¬ 𝑏 𝑅 𝑎 ) → ( ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) )
29 19 28 syl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ( ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) )
30 7 16 29 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 )
31 imassrn ⊢ ( 𝑠 “ { 𝑎 } ) ⊆ ran 𝑠
32 rnss ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) )
33 32 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ran 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ran 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) )
35 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
36 34 35 sstrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ran 𝑠 ⊆ 𝐵 )
37 31 36 sstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 )
38 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → 𝑎 ∈ dom 𝑠 )
39 imadisj ⊢ ( ( 𝑠 “ { 𝑎 } ) = ∅ ↔ ( dom 𝑠 ∩ { 𝑎 } ) = ∅ )
40 disjsn ⊢ ( ( dom 𝑠 ∩ { 𝑎 } ) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠 )
41 39 40 bitri ⊢ ( ( 𝑠 “ { 𝑎 } ) = ∅ ↔ ¬ 𝑎 ∈ dom 𝑠 )
42 41 necon2abii ⊢ ( 𝑎 ∈ dom 𝑠 ↔ ( 𝑠 “ { 𝑎 } ) ≠ ∅ )
43 38 42 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ( 𝑠 “ { 𝑎 } ) ≠ ∅ )
44 df-fr ⊢ ( 𝑆 Fr 𝐵 ↔ ∀ 𝑒 ( ( 𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑒 ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ) )
45 3 44 sylib ⊢ ( 𝜑 → ∀ 𝑒 ( ( 𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑒 ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ∀ 𝑒 ( ( 𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑒 ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ) )
47 20 imaex ⊢ ( 𝑠 “ { 𝑎 } ) ∈ V
48 sseq1 ⊢ ( 𝑒 = ( 𝑠 “ { 𝑎 } ) → ( 𝑒 ⊆ 𝐵 ↔ ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ) )
49 neeq1 ⊢ ( 𝑒 = ( 𝑠 “ { 𝑎 } ) → ( 𝑒 ≠ ∅ ↔ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) )
50 48 49 anbi12d ⊢ ( 𝑒 = ( 𝑠 “ { 𝑎 } ) → ( ( 𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅ ) ↔ ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) ) )
51 raleq ⊢ ( 𝑒 = ( 𝑠 “ { 𝑎 } ) → ( ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ↔ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) )
52 51 rexeqbi1dv ⊢ ( 𝑒 = ( 𝑠 “ { 𝑎 } ) → ( ∃ 𝑐 ∈ 𝑒 ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ↔ ∃ 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) )
53 50 52 imbi12d ⊢ ( 𝑒 = ( 𝑠 “ { 𝑎 } ) → ( ( ( 𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑒 ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ) ↔ ( ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) → ∃ 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) )
54 47 53 spcv ⊢ ( ∀ 𝑒 ( ( 𝑒 ⊆ 𝐵 ∧ 𝑒 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑒 ∀ 𝑑 ∈ 𝑒 ¬ 𝑑 𝑆 𝑐 ) → ( ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) → ∃ 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) )
55 46 54 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ( ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) → ∃ 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) )
56 37 43 55 mp2and ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ∃ 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 )
57 breq2 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑐 ⟩ → ( 𝑞 𝑇 𝑝 ↔ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
58 57 notbid ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑐 ⟩ → ( ¬ 𝑞 𝑇 𝑝 ↔ ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
59 58 ralbidv ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑐 ⟩ → ( ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ↔ ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
60 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) )
61 vex ⊢ 𝑎 ∈ V
62 vex ⊢ 𝑐 ∈ V
63 61 62 elimasn ⊢ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑐 ⟩ ∈ 𝑠 )
64 60 63 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ⟨ 𝑎 , 𝑐 ⟩ ∈ 𝑠 )
65 12 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → Rel 𝑠 )
66 elrel ⊢ ( ( Rel 𝑠 ∧ 𝑞 ∈ 𝑠 ) → ∃ 𝑒 ∃ 𝑓 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ )
67 65 66 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ∃ 𝑒 ∃ 𝑓 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ )
68 breq1 ⊢ ( 𝑑 = 𝑓 → ( 𝑑 𝑆 𝑐 ↔ 𝑓 𝑆 𝑐 ) )
69 68 notbid ⊢ ( 𝑑 = 𝑓 → ( ¬ 𝑑 𝑆 𝑐 ↔ ¬ 𝑓 𝑆 𝑐 ) )
70 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 )
71 vex ⊢ 𝑓 ∈ V
72 61 71 elimasn ⊢ ( 𝑓 ∈ ( 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 )
73 72 bilanri ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → 𝑓 ∈ ( 𝑠 “ { 𝑎 } ) )
74 69 70 73 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ 𝑓 𝑆 𝑐 )
75 74 intnanrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) )
76 opeq1 ⊢ ( 𝑒 = 𝑎 → ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝑎 , 𝑓 ⟩ )
77 76 eleq1d ⊢ ( 𝑒 = 𝑎 → ( ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ↔ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) )
78 77 anbi2d ⊢ ( 𝑒 = 𝑎 → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) ) )
79 3anass ⊢ ( ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
80 olc ⊢ ( 𝑒 = 𝑎 → ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) )
81 80 biantrurd ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
82 neeq1 ⊢ ( 𝑒 = 𝑎 → ( 𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
83 82 orbi1d ⊢ ( 𝑒 = 𝑎 → ( ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
84 neirr ⊢ ¬ 𝑎 ≠ 𝑎
85 84 biorfi ⊢ ( 𝑓 ≠ 𝑐 ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) )
86 83 85 bitr4di ⊢ ( 𝑒 = 𝑎 → ( ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ↔ 𝑓 ≠ 𝑐 ) )
87 86 anbi2d ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ 𝑓 ≠ 𝑐 ) ) )
88 andir ⊢ ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ 𝑓 ≠ 𝑐 ) ↔ ( ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ∨ ( 𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
89 nonconne ⊢ ¬ ( 𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐 )
90 89 biorfri ⊢ ( ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ↔ ( ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ∨ ( 𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
91 88 90 bitr4i ⊢ ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ 𝑓 ≠ 𝑐 ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) )
92 87 91 bitrdi ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
93 81 92 bitr3d ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
94 79 93 bitrid ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
95 94 notbid ⊢ ( 𝑒 = 𝑎 → ( ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ¬ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
96 78 95 imbi12d ⊢ ( 𝑒 = 𝑎 → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) ) )
97 75 96 mpbiri ⊢ ( 𝑒 = 𝑎 → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
98 97 impcom ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 = 𝑎 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
99 breq1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 𝑅 𝑎 ↔ 𝑒 𝑅 𝑎 ) )
100 99 notbid ⊢ ( 𝑏 = 𝑒 → ( ¬ 𝑏 𝑅 𝑎 ↔ ¬ 𝑒 𝑅 𝑎 ) )
101 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 )
102 101 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 )
103 vex ⊢ 𝑒 ∈ V
104 103 71 opeldm ⊢ ( ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠 )
105 104 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → 𝑒 ∈ dom 𝑠 )
106 105 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → 𝑒 ∈ dom 𝑠 )
107 100 102 106 rspcdva ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ 𝑒 𝑅 𝑎 )
108 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → 𝑒 ≠ 𝑎 )
109 108 neneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ 𝑒 = 𝑎 )
110 ioran ⊢ ( ¬ ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ↔ ( ¬ 𝑒 𝑅 𝑎 ∧ ¬ 𝑒 = 𝑎 ) )
111 107 109 110 sylanbrc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) )
112 111 intn3an1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
113 98 112 pm2.61dane ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
114 113 intn3an3d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
115 eleq1 ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑞 ∈ 𝑠 ↔ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) )
116 115 anbi2d ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ) )
117 breq1 ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ⟨ 𝑒 , 𝑓 ⟩ 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
118 1 xpord2lem ⊢ ( ⟨ 𝑒 , 𝑓 ⟩ 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
119 117 118 bitrdi ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
120 119 notbid ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ¬ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
121 116 120 imbi12d ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) ) )
122 114 121 mpbiri ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
123 122 com12 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
124 123 exlimdvv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( ∃ 𝑒 ∃ 𝑓 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
125 67 124 mpd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ )
126 125 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ )
127 59 64 126 rspcedvdw ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
128 56 127 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
129 30 128 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
130 129 ex ⊢ ( 𝜑 → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ) )
131 130 alrimiv ⊢ ( 𝜑 → ∀ 𝑠 ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ) )
132 df-fr ⊢ ( 𝑇 Fr ( 𝐴 × 𝐵 ) ↔ ∀ 𝑠 ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ) )
133 131 132 sylibr ⊢ ( 𝜑 → 𝑇 Fr ( 𝐴 × 𝐵 ) )