Theorem soseq 8154

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 5574	. . . 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 8153	. 2 ⊢ 𝑆 Po 𝐹
7		eleq1w 2843	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
8	7	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
9		fveq1 6872	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
10	9	eqeq1d 2762	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
11	10	ralbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
12		fveq1 6872	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
13	12	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
14	11, 13	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
15	14	rexbidv 3186	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
16	8, 15	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
17		eleq1w 2843	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
18	17	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
19		fveq1 6872	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
20	19	eqeq2d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
21	20	ralbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦)))
22		fveq1 6872	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑥) = (𝑏‘𝑥))
23	22	breq2d 5114	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))
24	21, 23	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
25	24	rexbidv 3186	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
26	18, 25	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
27	16, 26, 5	brabg 5510	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
28	27	bianabs 551	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
29		eleq1w 2843	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
30	29	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
31		fveq1 6872	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
32	31	eqeq1d 2762	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
33	32	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦)))
34		fveq1 6872	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑥) = (𝑏‘𝑥))
35	34	breq1d 5112	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))
36	33, 35	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
37	36	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
38	30, 37	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))))
39		eleq1w 2843	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
40	39	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
41		fveq1 6872	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
42	41	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦)))
43	42	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦)))
44		fveq1 6872	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
45	44	breq2d 5114	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
46	43, 45	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
47	46	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
48	40, 47	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
49	38, 48, 5	brabg 5510	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
50	49	bianabs 551	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
51	50	ancoms 464	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
52	28, 51	orbi12d 932	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
53	52	notbid 321	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
54		ralinexa 3115	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
55		andi 1025	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
56		eqcom 2767	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦))
57	56	ralbii 3108	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦))
58	57	anbi1i 636	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
59	58	orbi2i 926	. . . . . . . . . . 11 ⊢ (((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
60	55, 59	bitri 278	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
61	60	rexbii 3109	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
62		r19.43 3130	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
63	61, 62	bitri 278	. . . . . . . 8 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
64	54, 63	xchbinx 337	. . . . . . 7 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
65		feq2 6676	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑦⟶𝐴))
66	65	cbvrexvw 3241	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴)
67	66	abbii 2827	. . . . . . . . . . . . 13 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
68	4, 67	eqtri 2783	. . . . . . . . . . . 12 ⊢ 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
69	68	orderseqlem 8152	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
70	68	orderseqlem 8152	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))
71		sotrieq 5586	. . . . . . . . . . . 12 ⊢ ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
72	1, 71	mpan 703	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
73	69, 70, 72	syl2an 608	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
74	73	imbi2d 343	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
75	74	ralbidv 3185	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
76		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
77		fveq2 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑎‘𝑥) = (𝑎‘𝑦))
78		fveq2 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑏‘𝑥) = (𝑏‘𝑦))
79	77, 78	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
80	76, 79	sbcie 3779	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦))
81	80	ralbii 3108	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦))
82	81	imbi1i 352	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
83	82	ralbii 3108	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
84		tfisg 7848	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
85	83, 84	sylbir 238	. . . . . . . . 9 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
86		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑎 ∈ V
87		feq1 6675	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓:𝑥⟶𝐴 ↔ 𝑎:𝑥⟶𝐴))
88	87	rexbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴))
89	86, 88, 4	elab2 3635	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴)
90		feq2 6676	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑝 → (𝑎:𝑥⟶𝐴 ↔ 𝑎:𝑝⟶𝐴))
91	90	cbvrexvw 3241	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑎:𝑥⟶𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
92	89, 91	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
93		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
94		feq1 6675	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑏:𝑥⟶𝐴))
95	94	rexbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴))
96	93, 95, 4	elab2 3635	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴)
97		feq2 6676	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑏:𝑥⟶𝐴 ↔ 𝑏:𝑞⟶𝐴))
98	97	cbvrexvw 3241	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑏:𝑥⟶𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
99	96, 98	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
100	92, 99	anbi12i 640	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
101		reeanv 3234	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
102	100, 101	bitr4i 281	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴))
103		onss 7782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ On → 𝑞 ⊆ On)
104		ssralv 3999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
105	103, 104	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
106	105	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
107		soseq.4	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ ∅ ∈ 𝐴
108		fveq2 6873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑎‘𝑥) = (𝑎‘𝑝))
109		fveq2 6873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑏‘𝑥) = (𝑏‘𝑝))
110	108, 109	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑝 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑝) = (𝑏‘𝑝)))
111	110	rspcv 3572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝)))
112	111	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝))))
113		ffvelcdm 7069	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → (𝑏‘𝑝) ∈ 𝐴)
114		fdm 6707	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎:𝑝⟶𝐴 → dom 𝑎 = 𝑝)
115		eloni 6361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑝 ∈ On → Ord 𝑝)
116		ordirr 6369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
117	115, 116	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑝 ∈ On → ¬ 𝑝 ∈ 𝑝)
118		eleq2 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎 ↔ 𝑝 ∈ 𝑝))
119	118	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝 ∈ 𝑝))
120	119	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑝 ∈ 𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121	117, 120	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122		ndmfv 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑝 ∈ dom 𝑎 → (𝑎‘𝑝) = ∅)
123		eqtr2 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ∅ = (𝑏‘𝑝))
124		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∅ = (𝑏‘𝑝) → (∅ ∈ 𝐴 ↔ (𝑏‘𝑝) ∈ 𝐴))
125	124	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∅ = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126	123, 125	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127	126	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎‘𝑝) = ∅ → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128	121, 122, 127	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129	128	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
130	114, 129	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ On ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
131	130	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
132	113, 131	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
133	132	exp4b 436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))))
134	133	imp32 424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
135	112, 134	syldd 73	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
136	135	com23 87	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴)))
137	136	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴))
138	107, 137	mtoi 202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑝 ∈ 𝑞)
139	138	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
140	106, 139	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
141		onss 7782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ On → 𝑝 ⊆ On)
142		ssralv 3999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
143	141, 142	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
144	143	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
145		fveq2 6873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑎‘𝑥) = (𝑎‘𝑞))
146		fveq2 6873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑏‘𝑥) = (𝑏‘𝑞))
147	145, 146	eqeq12d 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑞 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑞) = (𝑏‘𝑞)))
148	147	rspcv 3572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞)))
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞))))
150		ffvelcdm 7069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → (𝑎‘𝑞) ∈ 𝐴)
151		fdm 6707	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏:𝑞⟶𝐴 → dom 𝑏 = 𝑞)
152		eloni 6361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑞 ∈ On → Ord 𝑞)
153		ordirr 6369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
154	152, 153	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑞 ∈ On → ¬ 𝑞 ∈ 𝑞)
155		eleq2 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏 ↔ 𝑞 ∈ 𝑞))
156	155	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞 ∈ 𝑞))
157	156	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158		ndmfv 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ 𝑞 ∈ dom 𝑏 → (𝑏‘𝑞) = ∅)
159	157, 158	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
160	154, 159	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
161		eqtr 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → (𝑎‘𝑞) = ∅)
162		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163	162	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164	161, 163	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165	164	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) = (𝑏‘𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166	165	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
167	160, 166	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
168	167	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
169	151, 168	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
170	150, 169	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
171	170	exp4b 436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞⟶𝐴 → (𝑎:𝑝⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
172	171	com23 87	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
173	172	imp32 424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
174	149, 173	syldd 73	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
175	174	com23 87	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴)))
176	175	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴))
177	107, 176	mtoi 202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑞 ∈ 𝑝)
178	177	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
179	144, 178	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
180	140, 179	jcad 522	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝)))
181		ordtri3or 6384	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
182	115, 152, 181	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
183	182	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
184		3orel13 1518	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝) → ((𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝) → 𝑝 = 𝑞))
185	180, 183, 184	syl6ci 72	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑝 = 𝑞))
186	185, 144	jcad 522	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
187		ffn 6697	. . . . . . . . . . . . . . 15 ⊢ (𝑎:𝑝⟶𝐴 → 𝑎 Fn 𝑝)
188		ffn 6697	. . . . . . . . . . . . . . 15 ⊢ (𝑏:𝑞⟶𝐴 → 𝑏 Fn 𝑞)
189		eqfnfv2 7018	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝑝 ∧ 𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
190	187, 188, 189	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
191	190	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
192	186, 191	sylibrd 262	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
193	192	ex 418	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)))
194	193	rexlimivv 3204	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
195	102, 194	sylbi 220	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
196	85, 195	syl5 35	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → 𝑎 = 𝑏))
197	75, 196	sylbird 263	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
198	64, 197	biimtrrid 246	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
199	53, 198	sylbid 243	. . . . 5 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) → 𝑎 = 𝑏))
200	199	orrd 877	. . . 4 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201		3orcomb 1110	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏))
202		df-3or 1104	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203	201, 202	bitr2i 279	. . . 4 ⊢ (((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
204	200, 203	sylib 221	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
205	204	rgen2 3202	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)
206		df-so 5556	. 2 ⊢ (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)))
207	6, 205, 206	mpbir2an 724	1 ⊢ 𝑆 Or 𝐹

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  [wsbc 3738   ∪ cun 3896   ⊆ wss 3898  ∅c0 4278  {csn 4583   class class class wbr 5102  {copab 5166   Po wpo 5553   Or wor 5554  dom cdm 5647  Ord word 6350  Oncon0 6351   Fn wfn 6522  ⟶wf 6523  ‘cfv 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6354  df-on 6355  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535

This theorem is used by:  ltsso  27966