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 ( 𝐴 × 𝐵 ) )