Theorem frxp 7967

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 4334	. . . . . . . . 9 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2		xpnz 6062	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
3	2	biimpri 227	. . . . . . . . . 10 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
4	3	simprd 496	. . . . . . . . 9 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
5	1, 4	syl 17	. . . . . . . 8 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6		dmxp 5838	. . . . . . . . . 10 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7		dmss 5811	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8		sseq2 3947	. . . . . . . . . . 11 ⊢ (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠 ⊆ 𝐴))
9	7, 8	syl5ib 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 5607	. . . . . . . . . . 11 ⊢ Rel (𝐴 × 𝐵)
14		relss 5692	. . . . . . . . . . 11 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
15	13, 14	mpi 20	. . . . . . . . . 10 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16		reldm0 5837	. . . . . . . . . 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 5544	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎))
22		vex 3436	. . . . . . . . 9 ⊢ 𝑠 ∈ V
23	22	dmex 7758	. . . . . . . 8 ⊢ dom 𝑠 ∈ V
24		sseq1 3946	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ⊆ 𝐴 ↔ dom 𝑠 ⊆ 𝐴))
25		neeq1 3006	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
26	24, 25	anbi12d 631	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → ((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) ↔ (dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅)))
27		raleq 3342	. . . . . . . . . 10 ⊢ (𝑣 = dom 𝑠 → (∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
28	27	rexeqbi1dv 3341	. . . . . . . . 9 ⊢ (𝑣 = dom 𝑠 → (∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
29	26, 28	imbi12d 345	. . . . . . . 8 ⊢ (𝑣 = dom 𝑠 → (((𝑣 ⊆ 𝐴 ∧ 𝑣 ≠ ∅) → ∃𝑎 ∈ 𝑣 ∀𝑐 ∈ 𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠 ⊆ 𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
30	23, 29	spcv 3544	. . . . . . 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 5980	. . . . . . . . . . . . . . 15 ⊢ (𝑠 “ {𝑎}) ⊆ ran 𝑠
35		xpeq0 6063	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
36	35	biimpri 227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
37	36	orcs 872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38		sseq2 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39		ss0 4332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ⊆ ∅ → 𝑠 = ∅)
40	38, 39	syl6bi 252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42		rneq 5845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = ∅ → ran 𝑠 = ran ∅)
43		rn0 5835	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ∅ = ∅
44		0ss 4330	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ⊆ 𝐵
45	43, 44	eqsstri 3955	. . . . . . . . . . . . . . . . . 18 ⊢ ran ∅ ⊆ 𝐵
46	42, 45	eqsstrdi 3975	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = ∅ → ran 𝑠 ⊆ 𝐵)
47	41, 46	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
48		rnxp 6073	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49		rnss 5848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50		sseq2 3947	. . . . . . . . . . . . . . . . . 18 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠 ⊆ 𝐵))
51	49, 50	syl5ib 243	. . . . . . . . . . . . . . . . 17 ⊢ (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵))
53	47, 52	pm2.61ine 3028	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ 𝐵)
54	34, 53	sstrid 3932	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
56	55	eldm 5809	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57		vex 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑏 ∈ V
58	55, 57	elimasn 5997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59		df-br 5075	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
60	58, 59	bitr4i 277	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61		ne0i 4268	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
62	60, 61	sylbir 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
63	62	exlimiv 1933	. . . . . . . . . . . . . . 15 ⊢ (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
64	56, 63	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65		df-fr 5544	. . . . . . . . . . . . . . 15 ⊢ (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏))
66	22	imaex 7763	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 “ {𝑎}) ∈ V
67		sseq1 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ⊆ 𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
69	67, 68	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → ((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70		raleq 3342	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
71	70	rexeqbi1dv 3341	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
72	69, 71	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (𝑠 “ {𝑎}) → (((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
73	66, 72	spcv 3544	. . . . . . . . . . . . . . 15 ⊢ (∀𝑣((𝑣 ⊆ 𝐵 ∧ 𝑣 ≠ ∅) → ∃𝑏 ∈ 𝑣 ∀𝑑 ∈ 𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
74	65, 73	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
75	54, 64, 74	syl2ani 607	. . . . . . . . . . . . 13 ⊢ (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76		1stdm 7881	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → (1st ‘𝑤) ∈ dom 𝑠)
77		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = (1st ‘𝑤) → (𝑐𝑅𝑎 ↔ (1st ‘𝑤)𝑅𝑎))
78	77	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = (1st ‘𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st ‘𝑤)𝑅𝑎))
79	78	rspccv 3558	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel 𝑠 ∧ 𝑤 ∈ 𝑠) → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
85	84	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Rel 𝑠 → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
86	85	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ∃𝑡∃𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑢 ∈ V
88	55, 87	elimasn 5997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 = 𝑢 → (𝑑𝑆𝑏 ↔ 𝑢𝑆𝑏))
90	89	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
91	90	rspccv 3558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
92	88, 91	syl5bir 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
93	92	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94		opeq1 4804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
95	94	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
96	95	imbi1d 342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
97	93, 96	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
98	97	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤 ∈ 𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑡 ∈ V
101	100, 87	op1std 7841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (1st ‘𝑤) = 𝑡)
102	101	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st ‘𝑤) = 𝑎 ↔ 𝑡 = 𝑎))
103	100, 87	op2ndd 7842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd ‘𝑤) = 𝑢)
104	103	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd ‘𝑤)𝑆𝑏 ↔ 𝑢𝑆𝑏))
105	104	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd ‘𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106	102, 105	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
107	99, 106	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))
113	83, 112	jcad 513	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤 ∈ 𝑠 → (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
114	113	ralrimiv 3102	. . . . . . . . . . . . . . . . . . . . 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 865	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
118	117	ralimi 3087	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝑠 (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)) → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
119	116, 118	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏)))))
120		ianor 979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
121		vex 3436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑤 ∈ V
122		opex 5379	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
123		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124	123	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → (1st ‘𝑥) = (1st ‘𝑤))
126	125	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅(1st ‘𝑦)))
127	125	eqeq1d 2740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((1st ‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑤) = (1st ‘𝑦)))
128		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (2nd ‘𝑥) = (2nd ‘𝑤))
129	128	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ((2nd ‘𝑥)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆(2nd ‘𝑦)))
130	127, 129	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑤 → (((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦))))
131	126, 130	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . 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 2826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134	133	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
135	55, 57	op1std 7841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (1st ‘𝑦) = 𝑎)
136	135	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤)𝑅(1st ‘𝑦) ↔ (1st ‘𝑤)𝑅𝑎))
137	135	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st ‘𝑤) = (1st ‘𝑦) ↔ (1st ‘𝑤) = 𝑎))
138	55, 57	op2ndd 7842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd ‘𝑦) = 𝑏)
139	138	breq2d 5086	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd ‘𝑤)𝑆(2nd ‘𝑦) ↔ (2nd ‘𝑤)𝑆𝑏))
140	137, 139	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st ‘𝑤) = (1st ‘𝑦) ∧ (2nd ‘𝑤)𝑆(2nd ‘𝑦)) ↔ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
141	136, 140	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . 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 5456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
145	120, 144	xchnxbir 333	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))))
146		ioran 981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)) ↔ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏)))
147		ianor 979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏) ↔ (¬ (1st ‘𝑤) = 𝑎 ∨ ¬ (2nd ‘𝑤)𝑆𝑏))
148		pm4.62 853	. . . . . . . . . . . . . . . . . . . . . . . 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 910	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st ‘𝑤)𝑅𝑎 ∨ ((1st ‘𝑤) = 𝑎 ∧ (2nd ‘𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
153	145, 152	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
154	153	ralbii 3092	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∀𝑤 ∈ 𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st ‘𝑤)𝑅𝑎 ∧ ((1st ‘𝑤) = 𝑎 → ¬ (2nd ‘𝑤)𝑆𝑏))))
155	119, 154	syl6ibr 251	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
156	155	reximdv 3202	. . . . . . . . . . . . . . . 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 1131	. . . . . . . . 9 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
164		resss 5916	. . . . . . . . . 10 ⊢ (𝑠 ↾ {𝑎}) ⊆ 𝑠
165		df-rex 3070	. . . . . . . . . . . . 13 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
166		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩
167		eqeq1 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧 ↔ 𝑤𝑇⟨𝑎, 𝑏⟩))
169	168	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
170	169	ralbidv 3112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))
171	170	anbi2d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)))
172	167, 171	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩))))
173	122, 172	spcev 3545	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
174	166, 173	mpan 687	. . . . . . . . . . . . . . 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 3070	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
181	55	elsnres 5931	. . . . . . . . . . . . . . 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 299	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
187	186	exbii 1850	. . . . . . . . . . . 12 ⊢ (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
188	180, 187	bitri 274	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)))
189	179, 188	sylibr 233	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇⟨𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧)
190		ssrexv 3988	. . . . . . . . . 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 3212	. . . . . 6 ⊢ ((𝑆 Fr 𝐵 ∧ 𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
195	194	3expib 1121	. . . . 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 5544	. 2 ⊢ (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧 ∈ 𝑠 ∀𝑤 ∈ 𝑠 ¬ 𝑤𝑇𝑧))
200	198, 199	sylibr 233	1 ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065   ⊆ wss 3887  ∅c0 4256  {csn 4561  ⟨cop 4567   class class class wbr 5074  {copab 5136   Fr wfr 5541   × cxp 5587  dom cdm 5589  ran crn 5590   ↾ cres 5591   “ cima 5592  Rel wrel 5594  ‘cfv 6433  1^st c1st 7829  2^nd c2nd 7830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-fr 5544  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-1st 7831  df-2nd 7832

This theorem is referenced by:  wexp  7971