This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frxp

Description: A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013) (Proof shortened by Wolf Lammen, 4-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 frxp.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) }
2 ssn0 ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( 𝐴 × 𝐵 ) ≠ ∅ )
3 xpnz ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
4 3 biimpri ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
5 4 simprd ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → 𝐵 ≠ ∅ )
6 2 5 syl ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → 𝐵 ≠ ∅ )
7 dmxp ⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
8 dmss ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → dom 𝑠 ⊆ dom ( 𝐴 × 𝐵 ) )
9 sseq2 ⊢ ( dom ( 𝐴 × 𝐵 ) = 𝐴 → ( dom 𝑠 ⊆ dom ( 𝐴 × 𝐵 ) ↔ dom 𝑠 ⊆ 𝐴 ) )
10 8 9 imbitrid ⊢ ( dom ( 𝐴 × 𝐵 ) = 𝐴 → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → dom 𝑠 ⊆ 𝐴 ) )
11 7 10 syl ⊢ ( 𝐵 ≠ ∅ → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → dom 𝑠 ⊆ 𝐴 ) )
12 11 impcom ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝐵 ≠ ∅ ) → dom 𝑠 ⊆ 𝐴 )
13 6 12 syldan ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → dom 𝑠 ⊆ 𝐴 )
14 relxp ⊢ Rel ( 𝐴 × 𝐵 )
15 relss ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( Rel ( 𝐴 × 𝐵 ) → Rel 𝑠 ) )
16 14 15 mpi ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → Rel 𝑠 )
17 reldm0 ⊢ ( Rel 𝑠 → ( 𝑠 = ∅ ↔ dom 𝑠 = ∅ ) )
18 16 17 syl ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑠 = ∅ ↔ dom 𝑠 = ∅ ) )
19 18 necon3bid ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅ ) )
20 19 biimpa ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → dom 𝑠 ≠ ∅ )
21 13 20 jca ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) )
22 df-fr ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑣 ( ( 𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ¬ 𝑐 𝑅 𝑎 ) )
23 vex ⊢ 𝑠 ∈ V
24 23 dmex ⊢ dom 𝑠 ∈ V
25 sseq1 ⊢ ( 𝑣 = dom 𝑠 → ( 𝑣 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴 ) )
26 neeq1 ⊢ ( 𝑣 = dom 𝑠 → ( 𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅ ) )
27 25 26 anbi12d ⊢ ( 𝑣 = dom 𝑠 → ( ( 𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅ ) ↔ ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) ) )
28 raleq ⊢ ( 𝑣 = dom 𝑠 → ( ∀ 𝑐 ∈ 𝑣 ¬ 𝑐 𝑅 𝑎 ↔ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) )
29 28 rexeqbi1dv ⊢ ( 𝑣 = dom 𝑠 → ( ∃ 𝑎 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ¬ 𝑐 𝑅 𝑎 ↔ ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) )
30 27 29 imbi12d ⊢ ( 𝑣 = dom 𝑠 → ( ( ( 𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ¬ 𝑐 𝑅 𝑎 ) ↔ ( ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) ) )
31 24 30 spcv ⊢ ( ∀ 𝑣 ( ( 𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑣 ∀ 𝑐 ∈ 𝑣 ¬ 𝑐 𝑅 𝑎 ) → ( ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) )
32 22 31 sylbi ⊢ ( 𝑅 Fr 𝐴 → ( ( dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) )
33 21 32 syl5 ⊢ ( 𝑅 Fr 𝐴 → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) )
34 33 adantr ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵 ) → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) )
35 imassrn ⊢ ( 𝑠 “ { 𝑎 } ) ⊆ ran 𝑠
36 xpeq0 ⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )
37 36 biimpri ⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝐴 × 𝐵 ) = ∅ )
38 37 orcs ⊢ ( 𝐴 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
39 sseq2 ⊢ ( ( 𝐴 × 𝐵 ) = ∅ → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ↔ 𝑠 ⊆ ∅ ) )
40 ss0 ⊢ ( 𝑠 ⊆ ∅ → 𝑠 = ∅ )
41 39 40 biimtrdi ⊢ ( ( 𝐴 × 𝐵 ) = ∅ → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → 𝑠 = ∅ ) )
42 38 41 syl ⊢ ( 𝐴 = ∅ → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → 𝑠 = ∅ ) )
43 rneq ⊢ ( 𝑠 = ∅ → ran 𝑠 = ran ∅ )
44 rn0 ⊢ ran ∅ = ∅
45 0ss ⊢ ∅ ⊆ 𝐵
46 44 45 eqsstri ⊢ ran ∅ ⊆ 𝐵
47 43 46 eqsstrdi ⊢ ( 𝑠 = ∅ → ran 𝑠 ⊆ 𝐵 )
48 42 47 syl6 ⊢ ( 𝐴 = ∅ → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑠 ⊆ 𝐵 ) )
49 rnxp ⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
50 rnss ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) )
51 sseq2 ⊢ ( ran ( 𝐴 × 𝐵 ) = 𝐵 → ( ran 𝑠 ⊆ ran ( 𝐴 × 𝐵 ) ↔ ran 𝑠 ⊆ 𝐵 ) )
52 50 51 imbitrid ⊢ ( ran ( 𝐴 × 𝐵 ) = 𝐵 → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑠 ⊆ 𝐵 ) )
53 49 52 syl ⊢ ( 𝐴 ≠ ∅ → ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑠 ⊆ 𝐵 ) )
54 48 53 pm2.61ine ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ran 𝑠 ⊆ 𝐵 )
55 35 54 sstrid ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 )
56 vex ⊢ 𝑎 ∈ V
57 56 eldm ⊢ ( 𝑎 ∈ dom 𝑠 ↔ ∃ 𝑏 𝑎 𝑠 𝑏 )
58 vex ⊢ 𝑏 ∈ V
59 56 58 elimasn ⊢ ( 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 )
60 df-br ⊢ ( 𝑎 𝑠 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 )
61 59 60 bitr4i ⊢ ( 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ↔ 𝑎 𝑠 𝑏 )
62 ne0i ⊢ ( 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) → ( 𝑠 “ { 𝑎 } ) ≠ ∅ )
63 61 62 sylbir ⊢ ( 𝑎 𝑠 𝑏 → ( 𝑠 “ { 𝑎 } ) ≠ ∅ )
64 63 exlimiv ⊢ ( ∃ 𝑏 𝑎 𝑠 𝑏 → ( 𝑠 “ { 𝑎 } ) ≠ ∅ )
65 57 64 sylbi ⊢ ( 𝑎 ∈ dom 𝑠 → ( 𝑠 “ { 𝑎 } ) ≠ ∅ )
66 df-fr ⊢ ( 𝑆 Fr 𝐵 ↔ ∀ 𝑣 ( ( 𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑣 ∀ 𝑑 ∈ 𝑣 ¬ 𝑑 𝑆 𝑏 ) )
67 23 imaex ⊢ ( 𝑠 “ { 𝑎 } ) ∈ V
68 sseq1 ⊢ ( 𝑣 = ( 𝑠 “ { 𝑎 } ) → ( 𝑣 ⊆ 𝐵 ↔ ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ) )
69 neeq1 ⊢ ( 𝑣 = ( 𝑠 “ { 𝑎 } ) → ( 𝑣 ≠ ∅ ↔ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) )
70 68 69 anbi12d ⊢ ( 𝑣 = ( 𝑠 “ { 𝑎 } ) → ( ( 𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅ ) ↔ ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) ) )
71 raleq ⊢ ( 𝑣 = ( 𝑠 “ { 𝑎 } ) → ( ∀ 𝑑 ∈ 𝑣 ¬ 𝑑 𝑆 𝑏 ↔ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) )
72 71 rexeqbi1dv ⊢ ( 𝑣 = ( 𝑠 “ { 𝑎 } ) → ( ∃ 𝑏 ∈ 𝑣 ∀ 𝑑 ∈ 𝑣 ¬ 𝑑 𝑆 𝑏 ↔ ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) )
73 70 72 imbi12d ⊢ ( 𝑣 = ( 𝑠 “ { 𝑎 } ) → ( ( ( 𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑣 ∀ 𝑑 ∈ 𝑣 ¬ 𝑑 𝑆 𝑏 ) ↔ ( ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) ) )
74 67 73 spcv ⊢ ( ∀ 𝑣 ( ( 𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑣 ∀ 𝑑 ∈ 𝑣 ¬ 𝑑 𝑆 𝑏 ) → ( ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) )
75 66 74 sylbi ⊢ ( 𝑆 Fr 𝐵 → ( ( ( 𝑠 “ { 𝑎 } ) ⊆ 𝐵 ∧ ( 𝑠 “ { 𝑎 } ) ≠ ∅ ) → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) )
76 55 65 75 syl2ani ⊢ ( 𝑆 Fr 𝐵 → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑎 ∈ dom 𝑠 ) → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) )
77 1stdm ⊢ ( ( Rel 𝑠 ∧ 𝑤 ∈ 𝑠 ) → ( 1st ‘ 𝑤 ) ∈ dom 𝑠 )
78 breq1 ⊢ ( 𝑐 = ( 1st ‘ 𝑤 ) → ( 𝑐 𝑅 𝑎 ↔ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
79 78 notbid ⊢ ( 𝑐 = ( 1st ‘ 𝑤 ) → ( ¬ 𝑐 𝑅 𝑎 ↔ ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
80 79 rspccv ⊢ ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ( ( 1st ‘ 𝑤 ) ∈ dom 𝑠 → ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
81 77 80 syl5 ⊢ ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ( ( Rel 𝑠 ∧ 𝑤 ∈ 𝑠 ) → ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
82 81 expd ⊢ ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ( Rel 𝑠 → ( 𝑤 ∈ 𝑠 → ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) ) )
83 82 impcom ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ( 𝑤 ∈ 𝑠 → ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
84 83 adantr ⊢ ( ( ( Rel 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
85 elrel ⊢ ( ( Rel 𝑠 ∧ 𝑤 ∈ 𝑠 ) → ∃ 𝑡 ∃ 𝑢 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ )
86 85 ex ⊢ ( Rel 𝑠 → ( 𝑤 ∈ 𝑠 → ∃ 𝑡 ∃ 𝑢 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ ) )
87 86 adantr ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ∃ 𝑡 ∃ 𝑢 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ ) )
88 vex ⊢ 𝑢 ∈ V
89 56 88 elimasn ⊢ ( 𝑢 ∈ ( 𝑠 “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑠 )
90 breq1 ⊢ ( 𝑑 = 𝑢 → ( 𝑑 𝑆 𝑏 ↔ 𝑢 𝑆 𝑏 ) )
91 90 notbid ⊢ ( 𝑑 = 𝑢 → ( ¬ 𝑑 𝑆 𝑏 ↔ ¬ 𝑢 𝑆 𝑏 ) )
92 91 rspccv ⊢ ( ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ( 𝑢 ∈ ( 𝑠 “ { 𝑎 } ) → ¬ 𝑢 𝑆 𝑏 ) )
93 89 92 biimtrrid ⊢ ( ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ( ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑠 → ¬ 𝑢 𝑆 𝑏 ) )
94 93 adantl ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑠 → ¬ 𝑢 𝑆 𝑏 ) )
95 opeq1 ⊢ ( 𝑡 = 𝑎 → ⟨ 𝑡 , 𝑢 ⟩ = ⟨ 𝑎 , 𝑢 ⟩ )
96 95 eleq1d ⊢ ( 𝑡 = 𝑎 → ( ⟨ 𝑡 , 𝑢 ⟩ ∈ 𝑠 ↔ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑠 ) )
97 96 imbi1d ⊢ ( 𝑡 = 𝑎 → ( ( ⟨ 𝑡 , 𝑢 ⟩ ∈ 𝑠 → ¬ 𝑢 𝑆 𝑏 ) ↔ ( ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑠 → ¬ 𝑢 𝑆 𝑏 ) ) )
98 94 97 imbitrrid ⊢ ( 𝑡 = 𝑎 → ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( ⟨ 𝑡 , 𝑢 ⟩ ∈ 𝑠 → ¬ 𝑢 𝑆 𝑏 ) ) )
99 98 com3l ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( ⟨ 𝑡 , 𝑢 ⟩ ∈ 𝑠 → ( 𝑡 = 𝑎 → ¬ 𝑢 𝑆 𝑏 ) ) )
100 eleq1 ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 𝑤 ∈ 𝑠 ↔ ⟨ 𝑡 , 𝑢 ⟩ ∈ 𝑠 ) )
101 vex ⊢ 𝑡 ∈ V
102 101 88 op1std ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 1st ‘ 𝑤 ) = 𝑡 )
103 102 eqeq1d ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( 1st ‘ 𝑤 ) = 𝑎 ↔ 𝑡 = 𝑎 ) )
104 101 88 op2ndd ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 2nd ‘ 𝑤 ) = 𝑢 )
105 104 breq1d ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ↔ 𝑢 𝑆 𝑏 ) )
106 105 notbid ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ↔ ¬ 𝑢 𝑆 𝑏 ) )
107 103 106 imbi12d ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ↔ ( 𝑡 = 𝑎 → ¬ 𝑢 𝑆 𝑏 ) ) )
108 100 107 imbi12d ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( 𝑤 ∈ 𝑠 → ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ↔ ( ⟨ 𝑡 , 𝑢 ⟩ ∈ 𝑠 → ( 𝑡 = 𝑎 → ¬ 𝑢 𝑆 𝑏 ) ) ) )
109 99 108 imbitrrid ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
110 109 exlimivv ⊢ ( ∃ 𝑡 ∃ 𝑢 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
111 110 com3l ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ( ∃ 𝑡 ∃ 𝑢 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
112 87 111 mpdd ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
113 112 adantlr ⊢ ( ( ( Rel 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
114 84 113 jcad ⊢ ( ( ( Rel 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ( 𝑤 ∈ 𝑠 → ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
115 114 ralrimiv ⊢ ( ( ( Rel 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) ∧ ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 ) → ∀ 𝑤 ∈ 𝑠 ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
116 115 ex ⊢ ( ( Rel 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ( ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ∀ 𝑤 ∈ 𝑠 ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
117 16 116 sylan ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ( ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ∀ 𝑤 ∈ 𝑠 ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
118 olc ⊢ ( ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) → ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
119 118 ralimi ⊢ ( ∀ 𝑤 ∈ 𝑠 ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) → ∀ 𝑤 ∈ 𝑠 ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
120 117 119 syl6 ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ( ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ∀ 𝑤 ∈ 𝑠 ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) ) )
121 ianor ⊢ ( ¬ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) ↔ ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ¬ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
122 vex ⊢ 𝑤 ∈ V
123 opex ⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
124 eleq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ 𝑤 ∈ ( 𝐴 × 𝐵 ) ) )
125 124 anbi1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ) )
126 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑤 ) )
127 126 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑤 ) 𝑅 ( 1st ‘ 𝑦 ) ) )
128 126 eqeq1d ⊢ ( 𝑥 = 𝑤 → ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ) )
129 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑤 ) )
130 129 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) )
131 128 130 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ↔ ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) )
132 127 131 orbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ↔ ( ( 1st ‘ 𝑤 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) )
133 125 132 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑤 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) ) )
134 eleq1 ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
135 134 anbi2d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ) )
136 56 58 op1std ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1st ‘ 𝑦 ) = 𝑎 )
137 136 breq2d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1st ‘ 𝑤 ) 𝑅 ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ) )
138 136 eqeq2d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑤 ) = 𝑎 ) )
139 56 58 op2ndd ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑦 ) = 𝑏 )
140 139 breq2d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) )
141 138 140 anbi12d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ↔ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
142 137 141 orbi12d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1st ‘ 𝑤 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ↔ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
143 135 142 anbi12d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑤 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑤 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) ) )
144 122 123 133 143 1 brab ⊢ ( 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
145 121 144 xchnxbir ⊢ ( ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ¬ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
146 ioran ⊢ ( ¬ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ↔ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ¬ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
147 ianor ⊢ ( ¬ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ↔ ( ¬ ( 1st ‘ 𝑤 ) = 𝑎 ∨ ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) )
148 pm4.62 ⊢ ( ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ↔ ( ¬ ( 1st ‘ 𝑤 ) = 𝑎 ∨ ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) )
149 147 148 bitr4i ⊢ ( ¬ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ↔ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) )
150 149 anbi2i ⊢ ( ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ¬ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ↔ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
151 146 150 bitri ⊢ ( ¬ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ↔ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) )
152 151 orbi2i ⊢ ( ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ¬ ( ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∨ ( ( 1st ‘ 𝑤 ) = 𝑎 ∧ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) ↔ ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
153 145 152 bitri ⊢ ( ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
154 153 ralbii ⊢ ( ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ∀ 𝑤 ∈ 𝑠 ( ¬ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) ∨ ( ¬ ( 1st ‘ 𝑤 ) 𝑅 𝑎 ∧ ( ( 1st ‘ 𝑤 ) = 𝑎 → ¬ ( 2nd ‘ 𝑤 ) 𝑆 𝑏 ) ) ) )
155 120 154 imbitrrdi ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ( ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
156 155 reximdv ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
157 156 ex ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) )
158 157 com23 ⊢ ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) → ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) )
159 158 adantr ⊢ ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑎 ∈ dom 𝑠 ) → ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑑 ∈ ( 𝑠 “ { 𝑎 } ) ¬ 𝑑 𝑆 𝑏 → ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) )
160 76 159 sylcom ⊢ ( 𝑆 Fr 𝐵 → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑎 ∈ dom 𝑠 ) → ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) )
161 160 impl ⊢ ( ( ( 𝑆 Fr 𝐵 ∧ 𝑠 ⊆ ( 𝐴 × 𝐵 ) ) ∧ 𝑎 ∈ dom 𝑠 ) → ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
162 161 expimpd ⊢ ( ( 𝑆 Fr 𝐵 ∧ 𝑠 ⊆ ( 𝐴 × 𝐵 ) ) → ( ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
163 162 3adant3 ⊢ ( ( 𝑆 Fr 𝐵 ∧ 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
164 resss ⊢ ( 𝑠 ↾ { 𝑎 } ) ⊆ 𝑠
165 df-rex ⊢ ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ∃ 𝑏 ( 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
166 eqid ⊢ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 𝑏 ⟩
167 eqeq1 ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
168 breq2 ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑤 𝑇 𝑧 ↔ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
169 168 notbid ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( ¬ 𝑤 𝑇 𝑧 ↔ ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
170 169 ralbidv ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ↔ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
171 170 anbi2d ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) )
172 167 171 anbi12d ⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) ) )
173 123 172 spcev ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) → ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
174 166 173 mpan ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) → ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
175 59 174 sylanb ⊢ ( ( 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) → ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
176 175 eximi ⊢ ( ∃ 𝑏 ( 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) → ∃ 𝑏 ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
177 165 176 sylbi ⊢ ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑏 ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
178 excom ⊢ ( ∃ 𝑏 ∃ 𝑧 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) ↔ ∃ 𝑧 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
179 177 178 sylib ⊢ ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑧 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
180 df-rex ⊢ ( ∃ 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
181 56 elsnres ⊢ ( 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ↔ ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ) )
182 181 anbi1i ⊢ ( ( 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ( ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
183 19.41v ⊢ ( ∃ 𝑏 ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ( ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
184 anass ⊢ ( ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
185 184 exbii ⊢ ( ∃ 𝑏 ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
186 182 183 185 3bitr2i ⊢ ( ( 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
187 186 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ↔ ∃ 𝑧 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
188 180 187 bitri ⊢ ( ∃ 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ↔ ∃ 𝑧 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑠 ∧ ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
189 179 188 sylibr ⊢ ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 )
190 ssrexv ⊢ ( ( 𝑠 ↾ { 𝑎 } ) ⊆ 𝑠 → ( ∃ 𝑧 ∈ ( 𝑠 ↾ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
191 164 189 190 mpsyl ⊢ ( ∃ 𝑏 ∈ ( 𝑠 “ { 𝑎 } ) ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 ⟨ 𝑎 , 𝑏 ⟩ → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 )
192 163 191 syl6 ⊢ ( ( 𝑆 Fr 𝐵 ∧ 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( ( 𝑎 ∈ dom 𝑠 ∧ ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 ) → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
193 192 expd ⊢ ( ( 𝑆 Fr 𝐵 ∧ 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( 𝑎 ∈ dom 𝑠 → ( ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
194 193 rexlimdv ⊢ ( ( 𝑆 Fr 𝐵 ∧ 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
195 194 3expib ⊢ ( 𝑆 Fr 𝐵 → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
196 195 adantl ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵 ) → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ( ∃ 𝑎 ∈ dom 𝑠 ∀ 𝑐 ∈ dom 𝑠 ¬ 𝑐 𝑅 𝑎 → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) ) )
197 34 196 mpdd ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵 ) → ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
198 197 alrimiv ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵 ) → ∀ 𝑠 ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
199 df-fr ⊢ ( 𝑇 Fr ( 𝐴 × 𝐵 ) ↔ ∀ 𝑠 ( ( 𝑠 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑠 ≠ ∅ ) → ∃ 𝑧 ∈ 𝑠 ∀ 𝑤 ∈ 𝑠 ¬ 𝑤 𝑇 𝑧 ) )
200 198 199 sylibr ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵 ) → 𝑇 Fr ( 𝐴 × 𝐵 ) )