Metamath Proof Explorer

Theorem frxp2

Description: Another way of giving a founded order to a cross 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 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) )
58 vex ⊢ 𝑎 ∈ V
59 vex ⊢ 𝑐 ∈ V
60 58 59 elimasn ⊢ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑐 ⟩ ∈ 𝑠 )
61 57 60 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ⟨ 𝑎 , 𝑐 ⟩ ∈ 𝑠 )
62 12 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → Rel 𝑠 )
63 elrel ⊢ ( ( Rel 𝑠 ∧ 𝑞 ∈ 𝑠 ) → ∃ 𝑒 ∃ 𝑓 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ )
64 62 63 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ∃ 𝑒 ∃ 𝑓 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ )
65 breq1 ⊢ ( 𝑑 = 𝑓 → ( 𝑑 𝑆 𝑐 ↔ 𝑓 𝑆 𝑐 ) )
66 65 notbid ⊢ ( 𝑑 = 𝑓 → ( ¬ 𝑑 𝑆 𝑐 ↔ ¬ 𝑓 𝑆 𝑐 ) )
67 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 )
68 vex ⊢ 𝑓 ∈ V
69 58 68 elimasn ⊢ ( 𝑓 ∈ ( 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 )
70 69 biimpri ⊢ ( ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 → 𝑓 ∈ ( 𝑠 “ { 𝑎 } ) )
71 70 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → 𝑓 ∈ ( 𝑠 “ { 𝑎 } ) )
72 66 67 71 rspcdva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ 𝑓 𝑆 𝑐 )
73 72 intnanrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) )
74 opeq1 ⊢ ( 𝑒 = 𝑎 → ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝑎 , 𝑓 ⟩ )
75 74 eleq1d ⊢ ( 𝑒 = 𝑎 → ( ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ↔ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) )
76 75 anbi2d ⊢ ( 𝑒 = 𝑎 → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) ) )
77 3anass ⊢ ( ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
78 olc ⊢ ( 𝑒 = 𝑎 → ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) )
79 78 biantrurd ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
80 neeq1 ⊢ ( 𝑒 = 𝑎 → ( 𝑒 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
81 80 orbi1d ⊢ ( 𝑒 = 𝑎 → ( ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
82 neirr ⊢ ¬ 𝑎 ≠ 𝑎
83 biorf ⊢ ( ¬ 𝑎 ≠ 𝑎 → ( 𝑓 ≠ 𝑐 ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
84 82 83 ax-mp ⊢ ( 𝑓 ≠ 𝑐 ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) )
85 81 84 bitr4di ⊢ ( 𝑒 = 𝑎 → ( ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ↔ 𝑓 ≠ 𝑐 ) )
86 85 anbi2d ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ 𝑓 ≠ 𝑐 ) ) )
87 andir ⊢ ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ 𝑓 ≠ 𝑐 ) ↔ ( ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ∨ ( 𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
88 nonconne ⊢ ¬ ( 𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐 )
89 88 biorfi ⊢ ( ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ↔ ( ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ∨ ( 𝑓 = 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
90 87 89 bitr4i ⊢ ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ 𝑓 ≠ 𝑐 ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) )
91 86 90 bitrdi ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
92 79 91 bitr3d ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
93 77 92 syl5bb ⊢ ( 𝑒 = 𝑎 → ( ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
94 93 notbid ⊢ ( 𝑒 = 𝑎 → ( ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ¬ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) )
95 76 94 imbi12d ⊢ ( 𝑒 = 𝑎 → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑎 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( 𝑓 𝑆 𝑐 ∧ 𝑓 ≠ 𝑐 ) ) ) )
96 73 95 mpbiri ⊢ ( 𝑒 = 𝑎 → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
97 96 impcom ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 = 𝑎 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
98 breq1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 𝑅 𝑎 ↔ 𝑒 𝑅 𝑎 ) )
99 98 notbid ⊢ ( 𝑏 = 𝑒 → ( ¬ 𝑏 𝑅 𝑎 ↔ ¬ 𝑒 𝑅 𝑎 ) )
100 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 )
101 100 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 )
102 vex ⊢ 𝑒 ∈ V
103 102 68 opeldm ⊢ ( ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 → 𝑒 ∈ dom 𝑠 )
104 103 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → 𝑒 ∈ dom 𝑠 )
105 104 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → 𝑒 ∈ dom 𝑠 )
106 99 101 105 rspcdva ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ 𝑒 𝑅 𝑎 )
107 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → 𝑒 ≠ 𝑎 )
108 107 neneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ 𝑒 = 𝑎 )
109 ioran ⊢ ( ¬ ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ↔ ( ¬ 𝑒 𝑅 𝑎 ∧ ¬ 𝑒 = 𝑎 ) )
110 106 108 109 sylanbrc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) )
111 110 intn3an1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ∧ 𝑒 ≠ 𝑎 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
112 97 111 pm2.61dane ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) )
113 112 intn3an3d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
114 eleq1 ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑞 ∈ 𝑠 ↔ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) )
115 114 anbi2d ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) ↔ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) ) )
116 breq1 ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ⟨ 𝑒 , 𝑓 ⟩ 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
117 1 xpord2lem ⊢ ( ⟨ 𝑒 , 𝑓 ⟩ 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) )
118 116 117 bitrdi ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
119 118 notbid ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ↔ ¬ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
120 115 119 imbi12d ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) ↔ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ ⟨ 𝑒 , 𝑓 ⟩ ∈ 𝑠 ) → ¬ ( ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐵 ) ∧ ( ( 𝑒 𝑅 𝑎 ∨ 𝑒 = 𝑎 ) ∧ ( 𝑓 𝑆 𝑐 ∨ 𝑓 = 𝑐 ) ∧ ( 𝑒 ≠ 𝑎 ∨ 𝑓 ≠ 𝑐 ) ) ) ) ) )
121 113 120 mpbiri ⊢ ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
122 121 com12 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
123 122 exlimdvv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ( ∃ 𝑒 ∃ 𝑓 𝑞 = ⟨ 𝑒 , 𝑓 ⟩ → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
124 64 123 mpd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) ∧ 𝑞 ∈ 𝑠 ) → ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ )
125 124 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ )
126 breq2 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑐 ⟩ → ( 𝑞 𝑇 𝑝 ↔ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
127 126 notbid ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑐 ⟩ → ( ¬ 𝑞 𝑇 𝑝 ↔ ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
128 127 ralbidv ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑐 ⟩ → ( ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ↔ ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) )
129 128 rspcev ⊢ ( ( ⟨ 𝑎 , 𝑐 ⟩ ∈ 𝑠 ∧ ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 ⟨ 𝑎 , 𝑐 ⟩ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
130 61 125 129 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) ∧ ( 𝑐 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑐 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
131 56 130 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) ∧ ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑏 ∈ dom 𝑠 ¬ 𝑏 𝑅 𝑎 ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
132 30 131 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 )
133 132 ex ⊢ ( 𝜑 → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ) )
134 133 alrimiv ⊢ ( 𝜑 → ∀ 𝑠 ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ) )
135 df-fr ⊢ ( 𝑇 Fr ( 𝐴 × 𝐵 ) ↔ ∀ 𝑠 ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ¬ 𝑞 𝑇 𝑝 ) )
136 134 135 sylibr ⊢ ( 𝜑 → 𝑇 Fr ( 𝐴 × 𝐵 ) )