Theorem soseq 8184

Description: A linear ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypotheses

Ref	Expression
soseq.1	⊢ 𝑅 Or (𝐴 ∪ {∅})
soseq.2	⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}
soseq.3	⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
soseq.4	⊢ ¬ ∅ ∈ 𝐴

Assertion

Ref	Expression
soseq	⊢ 𝑆 Or 𝐹

Distinct variable groups:   𝐴,𝑓,𝑥,𝑦   𝑓,𝐹,𝑔,𝑥   𝑦,𝑓,𝑔,𝑥   𝑅,𝑓,𝑔,𝑥

Allowed substitution hints:   𝐴(𝑔)   𝑅(𝑦)   𝑆(𝑥,𝑦,𝑓,𝑔)   𝐹(𝑦)

Proof of Theorem soseq

Dummy variables 𝑎 𝑏 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		soseq.1	. . . 4 ⊢ 𝑅 Or (𝐴 ∪ {∅})
2		sopo 5611	. . . 4 ⊢ (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅}))
3	1, 2	ax-mp 5	. . 3 ⊢ 𝑅 Po (𝐴 ∪ {∅})
4		soseq.2	. . 3 ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴}
5		soseq.3	. . 3 ⊢ 𝑆 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))}
6	3, 4, 5	poseq 8183	. 2 ⊢ 𝑆 Po 𝐹
7		eleq1w 2824	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
8	7	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
9		fveq1 6905	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
10	9	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
11	10	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
12		fveq1 6905	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
13	12	breq1d 5153	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
14	11, 13	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
15	14	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
16	8, 15	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
17		eleq1w 2824	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
18	17	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
19		fveq1 6905	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
20	19	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
21	20	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦)))
22		fveq1 6905	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑥) = (𝑏‘𝑥))
23	22	breq2d 5155	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))
24	21, 23	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
25	24	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
26	18, 25	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
27	16, 26, 5	brabg 5544	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
28	27	bianabs 541	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
29		eleq1w 2824	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
30	29	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
31		fveq1 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
32	31	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
33	32	ralbidv 3178	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦)))
34		fveq1 6905	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑥) = (𝑏‘𝑥))
35	34	breq1d 5153	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))
36	33, 35	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
37	36	rexbidv 3179	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
38	30, 37	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))))
39		eleq1w 2824	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
40	39	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
41		fveq1 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
42	41	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦)))
43	42	ralbidv 3178	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦)))
44		fveq1 6905	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
45	44	breq2d 5155	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
46	43, 45	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
47	46	rexbidv 3179	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
48	40, 47	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
49	38, 48, 5	brabg 5544	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
50	49	bianabs 541	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
51	50	ancoms 458	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
52	28, 51	orbi12d 919	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
53	52	notbid 318	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
54		ralinexa 3101	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
55		andi 1010	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
56		eqcom 2744	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦))
57	56	ralbii 3093	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦))
58	57	anbi1i 624	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
59	58	orbi2i 913	. . . . . . . . . . 11 ⊢ (((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
60	55, 59	bitri 275	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
61	60	rexbii 3094	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
62		r19.43 3122	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
63	61, 62	bitri 275	. . . . . . . 8 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
64	54, 63	xchbinx 334	. . . . . . 7 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
65		feq2 6717	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑦⟶𝐴))
66	65	cbvrexvw 3238	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴)
67	66	abbii 2809	. . . . . . . . . . . . 13 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
68	4, 67	eqtri 2765	. . . . . . . . . . . 12 ⊢ 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
69	68	orderseqlem 8182	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
70	68	orderseqlem 8182	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))
71		sotrieq 5623	. . . . . . . . . . . 12 ⊢ ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
72	1, 71	mpan 690	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
73	69, 70, 72	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
74	73	imbi2d 340	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
75	74	ralbidv 3178	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
76		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
77		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑎‘𝑥) = (𝑎‘𝑦))
78		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑏‘𝑥) = (𝑏‘𝑦))
79	77, 78	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
80	76, 79	sbcie 3830	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦))
81	80	ralbii 3093	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦))
82	81	imbi1i 349	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
83	82	ralbii 3093	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
84		tfisg 7875	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
85	83, 84	sylbir 235	. . . . . . . . 9 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
86		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑎 ∈ V
87		feq1 6716	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓:𝑥⟶𝐴 ↔ 𝑎:𝑥⟶𝐴))
88	87	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴))
89	86, 88, 4	elab2 3682	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴)
90		feq2 6717	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑝 → (𝑎:𝑥⟶𝐴 ↔ 𝑎:𝑝⟶𝐴))
91	90	cbvrexvw 3238	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑎:𝑥⟶𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
92	89, 91	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
93		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
94		feq1 6716	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑏:𝑥⟶𝐴))
95	94	rexbidv 3179	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴))
96	93, 95, 4	elab2 3682	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴)
97		feq2 6717	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑏:𝑥⟶𝐴 ↔ 𝑏:𝑞⟶𝐴))
98	97	cbvrexvw 3238	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑏:𝑥⟶𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
99	96, 98	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
100	92, 99	anbi12i 628	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
101		reeanv 3229	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
102	100, 101	bitr4i 278	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴))
103		onss 7805	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ On → 𝑞 ⊆ On)
104		ssralv 4052	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
106	105	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
107		soseq.4	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ ∅ ∈ 𝐴
108		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑎‘𝑥) = (𝑎‘𝑝))
109		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑏‘𝑥) = (𝑏‘𝑝))
110	108, 109	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑝 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑝) = (𝑏‘𝑝)))
111	110	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝)))
112	111	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝))))
113		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → (𝑏‘𝑝) ∈ 𝐴)
114		fdm 6745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎:𝑝⟶𝐴 → dom 𝑎 = 𝑝)
115		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑝 ∈ On → Ord 𝑝)
116		ordirr 6402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑝 ∈ On → ¬ 𝑝 ∈ 𝑝)
118		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎 ↔ 𝑝 ∈ 𝑝))
119	118	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝 ∈ 𝑝))
120	119	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑝 ∈ 𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121	117, 120	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122		ndmfv 6941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑝 ∈ dom 𝑎 → (𝑎‘𝑝) = ∅)
123		eqtr2 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ∅ = (𝑏‘𝑝))
124		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∅ = (𝑏‘𝑝) → (∅ ∈ 𝐴 ↔ (𝑏‘𝑝) ∈ 𝐴))
125	124	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∅ = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126	123, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127	126	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎‘𝑝) = ∅ → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128	121, 122, 127	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129	128	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
130	114, 129	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ On ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
131	130	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
132	113, 131	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
133	132	exp4b 430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))))
134	133	imp32 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
135	112, 134	syldd 72	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
136	135	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴)))
137	136	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴))
138	107, 137	mtoi 199	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑝 ∈ 𝑞)
139	138	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
140	106, 139	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
141		onss 7805	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ On → 𝑝 ⊆ On)
142		ssralv 4052	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
144	143	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
145		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑎‘𝑥) = (𝑎‘𝑞))
146		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑏‘𝑥) = (𝑏‘𝑞))
147	145, 146	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑞 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑞) = (𝑏‘𝑞)))
148	147	rspcv 3618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞)))
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞))))
150		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → (𝑎‘𝑞) ∈ 𝐴)
151		fdm 6745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏:𝑞⟶𝐴 → dom 𝑏 = 𝑞)
152		eloni 6394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑞 ∈ On → Ord 𝑞)
153		ordirr 6402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
154	152, 153	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑞 ∈ On → ¬ 𝑞 ∈ 𝑞)
155		eleq2 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏 ↔ 𝑞 ∈ 𝑞))
156	155	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞 ∈ 𝑞))
157	156	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158		ndmfv 6941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ 𝑞 ∈ dom 𝑏 → (𝑏‘𝑞) = ∅)
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
160	154, 159	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
161		eqtr 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → (𝑎‘𝑞) = ∅)
162		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163	162	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165	164	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) = (𝑏‘𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166	165	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
167	160, 166	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
168	167	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
169	151, 168	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
170	150, 169	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
171	170	exp4b 430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞⟶𝐴 → (𝑎:𝑝⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
172	171	com23 86	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
173	172	imp32 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
174	149, 173	syldd 72	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
175	174	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴)))
176	175	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴))
177	107, 176	mtoi 199	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑞 ∈ 𝑝)
178	177	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
179	144, 178	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
180	140, 179	jcad 512	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝)))
181		ordtri3or 6416	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
182	115, 152, 181	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
183	182	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
184		3orel13 1489	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝) → ((𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝) → 𝑝 = 𝑞))
185	180, 183, 184	syl6ci 71	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑝 = 𝑞))
186	185, 144	jcad 512	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
187		ffn 6736	. . . . . . . . . . . . . . 15 ⊢ (𝑎:𝑝⟶𝐴 → 𝑎 Fn 𝑝)
188		ffn 6736	. . . . . . . . . . . . . . 15 ⊢ (𝑏:𝑞⟶𝐴 → 𝑏 Fn 𝑞)
189		eqfnfv2 7052	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝑝 ∧ 𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
190	187, 188, 189	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
191	190	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
192	186, 191	sylibrd 259	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
193	192	ex 412	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)))
194	193	rexlimivv 3201	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
195	102, 194	sylbi 217	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
196	85, 195	syl5 34	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → 𝑎 = 𝑏))
197	75, 196	sylbird 260	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
198	64, 197	biimtrrid 243	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
199	53, 198	sylbid 240	. . . . 5 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) → 𝑎 = 𝑏))
200	199	orrd 864	. . . 4 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201		3orcomb 1094	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏))
202		df-3or 1088	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203	201, 202	bitr2i 276	. . . 4 ⊢ (((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
204	200, 203	sylib 218	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
205	204	rgen2 3199	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)
206		df-so 5593	. 2 ⊢ (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)))
207	6, 205, 206	mpbir2an 711	1 ⊢ 𝑆 Or 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   = wceq 1540   ∈ wcel 2108  {cab 2714  ∀wral 3061  ∃wrex 3070  [wsbc 3788   ∪ cun 3949   ⊆ wss 3951  ∅c0 4333  {csn 4626   class class class wbr 5143  {copab 5205   Po wpo 5590   Or wor 5591  dom cdm 5685  Ord word 6383  Oncon0 6384   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  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-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  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-ord 6387  df-on 6388  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  sltso  27721