Theorem frxp 8151

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 4404	. . . . . . . . 9 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2		xpnz 6179	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
3	2	biimpri 228	. . . . . . . . . 10 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
4	3	simprd 495	. . . . . . . . 9 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
5	1, 4	syl 17	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6		dmxp 5939	. . . . . . . . . 10 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7		dmss 5913	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8		sseq2 4010	. . . . . . . . . . 11 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠 ⊆ 𝐴))
9	7, 8	imbitrid 244	. . . . . . . . . 10 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴))
10	6, 9	syl 17	. . . . . . . . 9 ⊢ (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴))
11	10	impcom 407	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠 ⊆ 𝐴)
12	5, 11	syldan 591	. . . . . . 7 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ⊆ 𝐴)
13		relxp 5703	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
14		relss 5791	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
15	13, 14	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16		reldm0 5938	. . . . . . . . . 10 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
17	15, 16	syl 17	. . . . . . . . 9 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
18	17	necon3bid 2985	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
19	18	biimpa 476	. . . . . . 7 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
20	12, 19	jca 511	. . . . . 6 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅))
21		df-fr 5637	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎))
22		vex 3484	. . . . . . . . 9 ⊢ 𝑠 ∈ V
23	22	dmex 7931	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
24		sseq1 4009	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
25		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
26	24, 25	anbi12d 632	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → ((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
27		raleq 3323	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
28	27	rexeqbi1dv 3339	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → (∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
29	26, 28	imbi12d 344	. . . . . . . 8 ⊢ (𝑣 = dom 𝑠 → (((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
30	23, 29	spcv 3605	. . . . . . 7 ⊢ (∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
31	21, 30	sylbi 217	. . . . . 6 ⊢ (𝑅 Fr 𝐴 → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
32	20, 31	syl5 34	. . . . 5 ⊢ (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
33	32	adantr 480	. . . 4 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34		imassrn 6089	. . . . . . . . . . . . . . 15 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
35		xpeq0 6180	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
36	35	biimpri 228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
37	36	orcs 876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38		sseq2 4010	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39		ss0 4402	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ ∅ → 𝑠 = ∅)
40	38, 39	biimtrdi 253	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42		rneq 5947	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = ∅ → ran 𝑠 = ran ∅)
43		rn0 5936	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ∅ = ∅
44		0ss 4400	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝐵
45	43, 44	eqsstri 4030	. . . . . . . . . . . . . . . . . 18 ⊢ ran ∅ ⊆ 𝐵
46	42, 45	eqsstrdi 4028	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = ∅ → ran 𝑠 ⊆ 𝐵)
47	41, 46	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
48		rnxp 6190	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49		rnss 5950	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50		sseq2 4010	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠 ⊆ 𝐵))
51	49, 50	imbitrid 244	. . . . . . . . . . . . . . . . 17 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
53	47, 52	pm2.61ine 3025	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)
54	34, 53	sstrid 3995	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55		vex 3484	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
56	55	eldm 5911	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57		vex 3484	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑏 ∈ V
58	55, 57	elimasn 6108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59		df-br 5144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
60	58, 59	bitr4i 278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61		ne0i 4341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
62	60, 61	sylbir 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
63	62	exlimiv 1930	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
64	56, 63	sylbi 217	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65		df-fr 5637	. . . . . . . . . . . . . . 15 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏))
66	22	imaex 7936	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 “ {𝑎}) ∈ V
67		sseq1 4009	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
69	67, 68	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → ((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70		raleq 3323	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
71	70	rexeqbi1dv 3339	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
72	69, 71	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
73	66, 72	spcv 3605	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
74	65, 73	sylbi 217	. . . . . . . . . . . . . 14 ⊢ (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
75	54, 64, 74	syl2ani 607	. . . . . . . . . . . . 13 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76		1stdm 8065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → (1st ‘𝑤) ∈ dom 𝑠)
77		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (1st ‘𝑤) → (𝑐𝑅𝑎 ↔ (1st ‘𝑤)𝑅𝑎))
78	77	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (1st ‘𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st ‘𝑤)𝑅𝑎))
79	78	rspccv 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st ‘𝑤) ∈ dom 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
80	76, 79	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ¬ (1st ‘𝑤)𝑅𝑎))
81	80	expd 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎)))
82	81	impcom 407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
83	82	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
84		elrel 5808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
85	84	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Rel 𝑠 → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
86	85	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑢 ∈ V
88	55, 87	elimasn 6108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = 𝑢 → (𝑑𝑆𝑏 ↔ 𝑢𝑆𝑏))
90	89	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
91	90	rspccv 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
92	88, 91	biimtrrid 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
93	92	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94		opeq1 4873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
95	94	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
96	95	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
97	93, 96	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
98	97	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤 ∈ 𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑡 ∈ V
101	100, 87	op1std 8024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (1st ‘𝑤) = 𝑡)
102	101	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 ↔ 𝑡 = 𝑎))
103	100, 87	op2ndd 8025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd ‘𝑤) = 𝑢)
104	103	breq1d 5153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd ‘𝑤)𝑆𝑏 ↔ 𝑢𝑆𝑏))
105	104	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd ‘𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106	102, 105	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
107	99, 106	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
108	98, 107	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
109	108	exlimivv 1932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
110	109	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
111	86, 110	mpdd 43	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
112	111	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
113	83, 112	jcad 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
114	113	ralrimiv 3145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
115	114	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
116	15, 115	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
117		olc 869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
118	117	ralimi 3083	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
119	116, 118	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))))
120		ianor 984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
121		vex 3484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
122		opex 5469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
123		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124	123	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤))
126	125	breq1d 5153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅(1st ‘𝑦)))
127	125	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑤) = (1st ‘𝑦)))
128		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤))
129	128	breq1d 5153	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))
130	127, 129	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))
131	126, 130	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))))
132	124, 131	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))))
133		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134	133	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
135	55, 57	op1std 8024	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (1st ‘𝑦) = 𝑎)
136	135	breq2d 5155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅𝑎))
137	135	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤) = (1st ‘𝑦) ↔ (1st ‘𝑤) = 𝑎))
138	55, 57	op2ndd 8025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
139	138	breq2d 5155	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑤)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆𝑏))
140	137, 139	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
141	136, 140	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
142	134, 141	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 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 5548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
145	120, 144	xchnxbir 333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
146		ioran 986	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
147		ianor 984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
148		pm4.62 857	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
149	147, 148	bitr4i 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))
150	149	anbi2i 623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
151	146, 150	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
152	151	orbi2i 913	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
153	145, 152	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
154	153	ralbii 3093	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
155	119, 154	imbitrrdi 252	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
156	155	reximdv 3170	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
157	156	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
158	157	com23 86	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
159	158	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
160	75, 159	sylcom 30	. . . . . . . . . . . 12 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
161	160	impl 455	. . . . . . . . . . 11 ⊢ (((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
162	161	expimpd 453	. . . . . . . . . 10 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
163	162	3adant3 1133	. . . . . . . . 9 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
164		resss 6019	. . . . . . . . . 10 ⊢ (𝑠 ↾ {𝑎}) ⊆ 𝑠
165		df-rex 3071	. . . . . . . . . . . . 13 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
166		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩
167		eqeq1 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168		breq2 5147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧 ↔ 𝑤𝑇⟨𝑎, 𝑏⟩))
169	168	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
170	169	ralbidv 3178	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
171	170	anbi2d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
172	167, 171	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))))
173	122, 172	spcev 3606	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
174	166, 173	mpan 690	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
175	58, 174	sylanb 581	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
176	175	eximi 1835	. . . . . . . . . . . . 13 ⊢ (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
177	165, 176	sylbi 217	. . . . . . . . . . . 12 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
178		excom 2162	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
179	177, 178	sylib 218	. . . . . . . . . . 11 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
180		df-rex 3071	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
181	55	elsnres 6039	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182	181	anbi1i 624	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
183		19.41v 1949	. . . . . . . . . . . . . 14 ⊢ (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
184		anass 468	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
185	184	exbii 1848	. . . . . . . . . . . . . 14 ⊢ (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
186	182, 183, 185	3bitr2i 299	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
187	186	exbii 1848	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
188	180, 187	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
189	179, 188	sylibr 234	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
190		ssrexv 4053	. . . . . . . . . 10 ⊢ ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
191	164, 189, 190	mpsyl 68	. . . . . . . . 9 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
192	163, 191	syl6 35	. . . . . . . 8 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
193	192	expd 415	. . . . . . 7 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
194	193	rexlimdv 3153	. . . . . 6 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
195	194	3expib 1123	. . . . 5 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
196	195	adantl 481	. . . 4 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
197	33, 196	mpdd 43	. . 3 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
198	197	alrimiv 1927	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
199		df-fr 5637	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
200	198, 199	sylibr 234	1 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ⊆ wss 3951  ∅c0 4333  {csn 4626  ⟨cop 4632   class class class wbr 5143  {copab 5205   Fr wfr 5634   × cxp 5683  dom cdm 5685  ran crn 5686   ↾ cres 5687   “ cima 5688  Rel wrel 5690  ‘cfv 6561  1^st c1st 8012  2^nd c2nd 8013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-fr 5637  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-2nd 8015

This theorem is referenced by:  wexp  8155