Theorem frxp 7174

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.)

Hypothesis

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

Assertion

Ref	Expression
frxp	⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝑇(𝑥,𝑦)

Proof of Theorem frxp

Dummy variables 𝑎 𝑏 𝑐 𝑠 𝑣 𝑤 𝑧 𝑑 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssn0 3928	. . . . . . . . 9 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2		xpnz 5472	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
3	2	biimpri 217	. . . . . . . . . 10 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
4	3	simprd 478	. . . . . . . . 9 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
5	1, 4	syl 17	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6		dmxp 5265	. . . . . . . . . 10 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7		dmss 5245	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8		sseq2 3590	. . . . . . . . . . 11 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠 ⊆ 𝐴))
9	7, 8	syl5ib 233	. . . . . . . . . 10 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴))
10	6, 9	syl 17	. . . . . . . . 9 ⊢ (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴))
11	10	impcom 445	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠 ⊆ 𝐴)
12	5, 11	syldan 486	. . . . . . 7 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ⊆ 𝐴)
13		relxp 5150	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
14		relss 5129	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
15	13, 14	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16		reldm0 5264	. . . . . . . . . 10 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
17	15, 16	syl 17	. . . . . . . . 9 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
18	17	necon3bid 2826	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
19	18	biimpa 500	. . . . . . 7 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
20	12, 19	jca 553	. . . . . 6 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅))
21		df-fr 4997	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎))
22		vex 3176	. . . . . . . . 9 ⊢ 𝑠 ∈ V
23	22	dmex 6991	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
24		sseq1 3589	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
25		neeq1 2844	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
26	24, 25	anbi12d 743	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → ((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
27		raleq 3115	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
28	27	rexeqbi1dv 3124	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → (∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
29	26, 28	imbi12d 333	. . . . . . . 8 ⊢ (𝑣 = dom 𝑠 → (((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
30	23, 29	spcv 3272	. . . . . . 7 ⊢ (∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
31	21, 30	sylbi 206	. . . . . 6 ⊢ (𝑅 Fr 𝐴 → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
32	20, 31	syl5 33	. . . . 5 ⊢ (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
33	32	adantr 480	. . . 4 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34		imassrn 5396	. . . . . . . . . . . . . . 15 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
35		xpeq0 5473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
36	35	biimpri 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
37	36	orcs 408	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38		sseq2 3590	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39		ss0 3926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ ∅ → 𝑠 = ∅)
40	38, 39	syl6bi 242	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42		rneq 5272	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = ∅ → ran 𝑠 = ran ∅)
43		rn0 5298	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ∅ = ∅
44		0ss 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝐵
45	43, 44	eqsstri 3598	. . . . . . . . . . . . . . . . . 18 ⊢ ran ∅ ⊆ 𝐵
46	42, 45	syl6eqss 3618	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = ∅ → ran 𝑠 ⊆ 𝐵)
47	41, 46	syl6 34	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
48		rnxp 5483	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49		rnss 5275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50		sseq2 3590	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠 ⊆ 𝐵))
51	49, 50	syl5ib 233	. . . . . . . . . . . . . . . . 17 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
53	47, 52	pm2.61ine 2865	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)
54	34, 53	syl5ss 3579	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55		vex 3176	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
56	55	eldm 5243	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑏 ∈ V
58	55, 57	elimasn 5409	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59		df-br 4584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
60	58, 59	bitr4i 266	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61		ne0i 3880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
62	60, 61	sylbir 224	. . . . . . . . . . . . . . . 16 ⊢ (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
63	62	exlimiv 1845	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
64	56, 63	sylbi 206	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65		df-fr 4997	. . . . . . . . . . . . . . 15 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏))
66	22	imaex 6996	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 “ {𝑎}) ∈ V
67		sseq1 3589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68		neeq1 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
69	67, 68	anbi12d 743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → ((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70		raleq 3115	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
71	70	rexeqbi1dv 3124	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
72	69, 71	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
73	66, 72	spcv 3272	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
74	65, 73	sylbi 206	. . . . . . . . . . . . . 14 ⊢ (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
75	54, 64, 74	syl2ani 686	. . . . . . . . . . . . 13 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76		1stdm 7106	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → (1st ‘𝑤) ∈ dom 𝑠)
77		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (1st ‘𝑤) → (𝑐𝑅𝑎 ↔ (1st ‘𝑤)𝑅𝑎))
78	77	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (1st ‘𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st ‘𝑤)𝑅𝑎))
79	78	rspccv 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st ‘𝑤) ∈ dom 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
80	76, 79	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ¬ (1st ‘𝑤)𝑅𝑎))
81	80	expd 451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎)))
82	81	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
83	82	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
84		elrel 5145	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
85	84	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Rel 𝑠 → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
86	85	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑢 ∈ V
88	55, 87	elimasn 5409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = 𝑢 → (𝑑𝑆𝑏 ↔ 𝑢𝑆𝑏))
90	89	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
91	90	rspccv 3279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
92	88, 91	syl5bir 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
93	92	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94		opeq1 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
95	94	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
96	95	imbi1d 330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
97	93, 96	syl5ibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
98	97	com3l 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤 ∈ 𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑡 ∈ V
101	100, 87	op1std 7069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (1st ‘𝑤) = 𝑡)
102	101	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 ↔ 𝑡 = 𝑎))
103	100, 87	op2ndd 7070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd ‘𝑤) = 𝑢)
104	103	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd ‘𝑤)𝑆𝑏 ↔ 𝑢𝑆𝑏))
105	104	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd ‘𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106	102, 105	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
107	99, 106	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
108	98, 107	syl5ibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
109	108	exlimivv 1847	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
110	109	com3l 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
111	86, 110	mpdd 42	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
112	111	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
113	83, 112	jcad 554	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
114	113	ralrimiv 2948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
115	114	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
116	15, 115	sylan 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
117		olc 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
118	117	ralimi 2936	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
119	116, 118	syl6 34	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))))
120		ianor 508	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
121		vex 3176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
122		opex 4859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
123		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124	123	anbi1d 737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤))
126	125	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅(1st ‘𝑦)))
127	125	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑤) = (1st ‘𝑦)))
128		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤))
129	128	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))
130	127, 129	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))
131	126, 130	orbi12d 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))))
132	124, 131	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))))
133		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134	133	anbi2d 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
135	55, 57	op1std 7069	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (1st ‘𝑦) = 𝑎)
136	135	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅𝑎))
137	135	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤) = (1st ‘𝑦) ↔ (1st ‘𝑤) = 𝑎))
138	55, 57	op2ndd 7070	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
139	138	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑤)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆𝑏))
140	137, 139	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
141	136, 140	orbi12d 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
142	134, 141	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))))
143		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))}
144	121, 122, 132, 142, 143	brab 4923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
145	120, 144	xchnxbir 322	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
146		ioran 510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
147		ianor 508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
148		pm4.62 434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
149	147, 148	bitr4i 266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))
150	149	anbi2i 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
151	146, 150	bitri 263	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
152	151	orbi2i 540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
153	145, 152	bitri 263	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
154	153	ralbii 2963	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
155	119, 154	syl6ibr 241	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
156	155	reximdv 2999	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
157	156	ex 449	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
158	157	com23 84	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
159	158	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
160	75, 159	sylcom 30	. . . . . . . . . . . 12 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
161	160	impl 648	. . . . . . . . . . 11 ⊢ (((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
162	161	expimpd 627	. . . . . . . . . 10 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
163	162	3adant3 1074	. . . . . . . . 9 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
164		resss 5342	. . . . . . . . . 10 ⊢ (𝑠 ↾ {𝑎}) ⊆ 𝑠
165		df-rex 2902	. . . . . . . . . . . . 13 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
166		eqid 2610	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩
167		eqeq1 2614	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168		breq2 4587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧 ↔ 𝑤𝑇⟨𝑎, 𝑏⟩))
169	168	notbid 307	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
170	169	ralbidv 2969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
171	170	anbi2d 736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
172	167, 171	anbi12d 743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))))
173	122, 172	spcev 3273	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
174	166, 173	mpan 702	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
175	58, 174	sylanb 488	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
176	175	eximi 1752	. . . . . . . . . . . . 13 ⊢ (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
177	165, 176	sylbi 206	. . . . . . . . . . . 12 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
178		excom 2029	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
179	177, 178	sylib 207	. . . . . . . . . . 11 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
180		df-rex 2902	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
181	55	elsnres 5356	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182	181	anbi1i 727	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
183		19.41v 1901	. . . . . . . . . . . . . 14 ⊢ (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
184		anass 679	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
185	184	exbii 1764	. . . . . . . . . . . . . 14 ⊢ (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
186	182, 183, 185	3bitr2i 287	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
187	186	exbii 1764	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
188	180, 187	bitri 263	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
189	179, 188	sylibr 223	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
190		ssrexv 3630	. . . . . . . . . 10 ⊢ ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
191	164, 189, 190	mpsyl 66	. . . . . . . . 9 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
192	163, 191	syl6 34	. . . . . . . 8 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
193	192	expd 451	. . . . . . 7 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
194	193	rexlimdv 3012	. . . . . 6 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
195	194	3expib 1260	. . . . 5 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
196	195	adantl 481	. . . 4 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
197	33, 196	mpdd 42	. . 3 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
198	197	alrimiv 1842	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
199		df-fr 4997	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
200	198, 199	sylibr 223	1 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∅c0 3874  {csn 4125  ⟨cop 4131   class class class wbr 4583  {copab 4642   Fr wfr 4994   × cxp 5036  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041  Rel wrel 5043  ‘cfv 5804  1^st c1st 7057  2^nd c2nd 7058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-int 4411  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-fr 4997  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fv 5812  df-1st 7059  df-2nd 7060

This theorem is referenced by:  wexp  7178