Theorem frxp 8058

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 4360	. . . . . . . . 9 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2		xpnz 6111	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
3	2	biimpri 227	. . . . . . . . . 10 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
4	3	simprd 496	. . . . . . . . 9 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
5	1, 4	syl 17	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6		dmxp 5884	. . . . . . . . . 10 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7		dmss 5858	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8		sseq2 3970	. . . . . . . . . . 11 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠 ⊆ 𝐴))
9	7, 8	imbitrid 243	. . . . . . . . . 10 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴))
10	6, 9	syl 17	. . . . . . . . 9 ⊢ (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ 𝐴))
11	10	impcom 408	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠 ⊆ 𝐴)
12	5, 11	syldan 591	. . . . . . 7 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ⊆ 𝐴)
13		relxp 5651	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
14		relss 5737	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
15	13, 14	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16		reldm0 5883	. . . . . . . . . 10 ⊢ (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
17	15, 16	syl 17	. . . . . . . . 9 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
18	17	necon3bid 2988	. . . . . . . 8 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
19	18	biimpa 477	. . . . . . 7 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
20	12, 19	jca 512	. . . . . 6 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅))
21		df-fr 5588	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎))
22		vex 3449	. . . . . . . . 9 ⊢ 𝑠 ∈ V
23	22	dmex 7848	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
24		sseq1 3969	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
25		neeq1 3006	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
26	24, 25	anbi12d 631	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → ((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
27		raleq 3309	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
28	27	rexeqbi1dv 3308	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → (∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
29	26, 28	imbi12d 344	. . . . . . . 8 ⊢ (𝑣 = dom 𝑠 → (((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
30	23, 29	spcv 3564	. . . . . . 7 ⊢ (∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
31	21, 30	sylbi 216	. . . . . 6 ⊢ (𝑅 Fr 𝐴 → ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
32	20, 31	syl5 34	. . . . 5 ⊢ (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
33	32	adantr 481	. . . 4 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34		imassrn 6024	. . . . . . . . . . . . . . 15 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
35		xpeq0 6112	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
36	35	biimpri 227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
37	36	orcs 873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38		sseq2 3970	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39		ss0 4358	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ ∅ → 𝑠 = ∅)
40	38, 39	syl6bi 252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42		rneq 5891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = ∅ → ran 𝑠 = ran ∅)
43		rn0 5881	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ∅ = ∅
44		0ss 4356	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝐵
45	43, 44	eqsstri 3978	. . . . . . . . . . . . . . . . . 18 ⊢ ran ∅ ⊆ 𝐵
46	42, 45	eqsstrdi 3998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = ∅ → ran 𝑠 ⊆ 𝐵)
47	41, 46	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
48		rnxp 6122	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49		rnss 5894	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50		sseq2 3970	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠 ⊆ 𝐵))
51	49, 50	imbitrid 243	. . . . . . . . . . . . . . . . 17 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
53	47, 52	pm2.61ine 3028	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)
54	34, 53	sstrid 3955	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55		vex 3449	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
56	55	eldm 5856	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57		vex 3449	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑏 ∈ V
58	55, 57	elimasn 6041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59		df-br 5106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
60	58, 59	bitr4i 277	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61		ne0i 4294	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
62	60, 61	sylbir 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
63	62	exlimiv 1933	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
64	56, 63	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65		df-fr 5588	. . . . . . . . . . . . . . 15 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏))
66	22	imaex 7853	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 “ {𝑎}) ∈ V
67		sseq1 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
69	67, 68	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → ((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70		raleq 3309	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
71	70	rexeqbi1dv 3308	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
72	69, 71	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
73	66, 72	spcv 3564	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
74	65, 73	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
75	54, 64, 74	syl2ani 607	. . . . . . . . . . . . 13 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76		1stdm 7972	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → (1st ‘𝑤) ∈ dom 𝑠)
77		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (1st ‘𝑤) → (𝑐𝑅𝑎 ↔ (1st ‘𝑤)𝑅𝑎))
78	77	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (1st ‘𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st ‘𝑤)𝑅𝑎))
79	78	rspccv 3578	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st ‘𝑤) ∈ dom 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
80	76, 79	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ¬ (1st ‘𝑤)𝑅𝑎))
81	80	expd 416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎)))
82	81	impcom 408	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
83	82	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ¬ (1st ‘𝑤)𝑅𝑎))
84		elrel 5754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
85	84	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Rel 𝑠 → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
86	85	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑢 ∈ V
88	55, 87	elimasn 6041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = 𝑢 → (𝑑𝑆𝑏 ↔ 𝑢𝑆𝑏))
90	89	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
91	90	rspccv 3578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
92	88, 91	biimtrrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
93	92	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94		opeq1 4830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
95	94	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
96	95	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
97	93, 96	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
98	97	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤 ∈ 𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100		vex 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑡 ∈ V
101	100, 87	op1std 7931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (1st ‘𝑤) = 𝑡)
102	101	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 ↔ 𝑡 = 𝑎))
103	100, 87	op2ndd 7932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd ‘𝑤) = 𝑢)
104	103	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd ‘𝑤)𝑆𝑏 ↔ 𝑢𝑆𝑏))
105	104	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd ‘𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106	102, 105	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
107	99, 106	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
108	98, 107	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
109	108	exlimivv 1935	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
110	109	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
111	86, 110	mpdd 43	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
112	111	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
113	83, 112	jcad 513	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
114	113	ralrimiv 3142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
115	114	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
116	15, 115	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
117		olc 866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
118	117	ralimi 3086	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
119	116, 118	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))))
120		ianor 980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
121		vex 3449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
122		opex 5421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
123		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124	123	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤))
126	125	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅(1st ‘𝑦)))
127	125	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑤) = (1st ‘𝑦)))
128		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤))
129	128	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))
130	127, 129	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))
131	126, 130	orbi12d 917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))))
132	124, 131	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))))
133		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134	133	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
135	55, 57	op1std 7931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (1st ‘𝑦) = 𝑎)
136	135	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅𝑎))
137	135	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤) = (1st ‘𝑦) ↔ (1st ‘𝑤) = 𝑎))
138	55, 57	op2ndd 7932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
139	138	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑤)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆𝑏))
140	137, 139	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
141	136, 140	orbi12d 917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))) ↔ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
142	134, 141	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 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 5500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
145	120, 144	xchnxbir 332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
146		ioran 982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
147		ianor 980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
148		pm4.62 854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
149	147, 148	bitr4i 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))
150	149	anbi2i 623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
151	146, 150	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
152	151	orbi2i 911	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
153	145, 152	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
154	153	ralbii 3096	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
155	119, 154	syl6ibr 251	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
156	155	reximdv 3167	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
157	156	ex 413	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
158	157	com23 86	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
159	158	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
160	75, 159	sylcom 30	. . . . . . . . . . . 12 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
161	160	impl 456	. . . . . . . . . . 11 ⊢ (((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
162	161	expimpd 454	. . . . . . . . . 10 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
163	162	3adant3 1132	. . . . . . . . 9 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
164		resss 5962	. . . . . . . . . 10 ⊢ (𝑠 ↾ {𝑎}) ⊆ 𝑠
165		df-rex 3074	. . . . . . . . . . . . 13 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
166		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩
167		eqeq1 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168		breq2 5109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧 ↔ 𝑤𝑇⟨𝑎, 𝑏⟩))
169	168	notbid 317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
170	169	ralbidv 3174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
171	170	anbi2d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
172	167, 171	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))))
173	122, 172	spcev 3565	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
174	166, 173	mpan 688	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
175	58, 174	sylanb 581	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
176	175	eximi 1837	. . . . . . . . . . . . 13 ⊢ (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩) → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
177	165, 176	sylbi 216	. . . . . . . . . . . 12 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
178		excom 2162	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
179	177, 178	sylib 217	. . . . . . . . . . 11 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
180		df-rex 3074	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
181	55	elsnres 5977	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182	181	anbi1i 624	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
183		19.41v 1953	. . . . . . . . . . . . . 14 ⊢ (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
184		anass 469	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
185	184	exbii 1850	. . . . . . . . . . . . . 14 ⊢ (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
186	182, 183, 185	3bitr2i 298	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
187	186	exbii 1850	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
188	180, 187	bitri 274	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
189	179, 188	sylibr 233	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
190		ssrexv 4011	. . . . . . . . . 10 ⊢ ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
191	164, 189, 190	mpsyl 68	. . . . . . . . 9 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
192	163, 191	syl6 35	. . . . . . . 8 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
193	192	expd 416	. . . . . . 7 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
194	193	rexlimdv 3150	. . . . . 6 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
195	194	3expib 1122	. . . . 5 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
196	195	adantl 482	. . . 4 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
197	33, 196	mpdd 43	. . 3 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
198	197	alrimiv 1930	. 2 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
199		df-fr 5588	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
200	198, 199	sylibr 233	1 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073   ⊆ wss 3910  ∅c0 4282  {csn 4586  ⟨cop 4592   class class class wbr 5105  {copab 5167   Fr wfr 5585   × cxp 5631  dom cdm 5633  ran crn 5634   ↾ cres 5635   “ cima 5636  Rel wrel 5638  ‘cfv 6496  1^st c1st 7919  2^nd c2nd 7920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-fr 5588  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922

This theorem is referenced by:  wexp  8062