Theorem soseq 30995

Description: A linear ordering of sequences of ordinals. (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 4976	. . . 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 30994	. 2 ⊢ 𝑆 Po 𝐹
7		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
8	7	anbi1d 737	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
9		fveq1 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
10	9	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
11	10	ralbidv 2969	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
12		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
13	12	breq1d 4593	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
14	11, 13	anbi12d 743	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
15	14	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
16	8, 15	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
17		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
18	17	anbi2d 736	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
19		fveq1 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
20	19	eqeq2d 2620	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
21	20	ralbidv 2969	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦)))
22		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑥) = (𝑏‘𝑥))
23	22	breq2d 4595	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))
24	21, 23	anbi12d 743	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
25	24	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
26	18, 25	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
27	16, 26, 5	brabg 4919	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
28	27	bianabs 920	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
29		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
30	29	anbi1d 737	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
31		fveq1 6102	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
32	31	eqeq1d 2612	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
33	32	ralbidv 2969	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦)))
34		fveq1 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑥) = (𝑏‘𝑥))
35	34	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))
36	33, 35	anbi12d 743	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
37	36	rexbidv 3034	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
38	30, 37	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))))
39		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
40	39	anbi2d 736	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
41		fveq1 6102	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
42	41	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦)))
43	42	ralbidv 2969	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦)))
44		fveq1 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
45	44	breq2d 4595	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
46	43, 45	anbi12d 743	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
47	46	rexbidv 3034	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
48	40, 47	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
49	38, 48, 5	brabg 4919	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
50	49	bianabs 920	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
51	50	ancoms 468	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
52	28, 51	orbi12d 742	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
53	52	notbid 307	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
54		ralinexa 2980	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
55		andi 907	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
56		eqcom 2617	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦))
57	56	ralbii 2963	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦))
58	57	anbi1i 727	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
59	58	orbi2i 540	. . . . . . . . . . 11 ⊢ (((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
60	55, 59	bitri 263	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
61	60	rexbii 3023	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
62		r19.43 3074	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
63	61, 62	bitri 263	. . . . . . . 8 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
64	54, 63	xchbinx 323	. . . . . . 7 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
65		feq2 5940	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑦⟶𝐴))
66	65	cbvrexv 3148	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴)
67	66	abbii 2726	. . . . . . . . . . . . 13 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
68	4, 67	eqtri 2632	. . . . . . . . . . . 12 ⊢ 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
69	68	orderseqlem 30993	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
70	68	orderseqlem 30993	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))
71		sotrieq 4986	. . . . . . . . . . . 12 ⊢ ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
72	1, 71	mpan 702	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
73	69, 70, 72	syl2an 493	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
74	73	imbi2d 329	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
75	74	ralbidv 2969	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
76		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
77		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑎‘𝑥) = (𝑎‘𝑦))
78		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑏‘𝑥) = (𝑏‘𝑦))
79	77, 78	eqeq12d 2625	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
80	76, 79	sbcie 3437	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦))
81	80	ralbii 2963	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦))
82	81	imbi1i 338	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
83	82	ralbii 2963	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
84		tfisg 30960	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
85	83, 84	sylbir 224	. . . . . . . . 9 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
86		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑎 ∈ V
87		feq1 5939	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓:𝑥⟶𝐴 ↔ 𝑎:𝑥⟶𝐴))
88	87	rexbidv 3034	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴))
89	86, 88, 4	elab2 3323	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴)
90		feq2 5940	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑝 → (𝑎:𝑥⟶𝐴 ↔ 𝑎:𝑝⟶𝐴))
91	90	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑎:𝑥⟶𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
92	89, 91	bitri 263	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
93		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
94		feq1 5939	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑏:𝑥⟶𝐴))
95	94	rexbidv 3034	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴))
96	93, 95, 4	elab2 3323	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴)
97		feq2 5940	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑏:𝑥⟶𝐴 ↔ 𝑏:𝑞⟶𝐴))
98	97	cbvrexv 3148	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑏:𝑥⟶𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
99	96, 98	bitri 263	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
100	92, 99	anbi12i 729	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
101		reeanv 3086	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
102	100, 101	bitr4i 266	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴))
103		onss 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ On → 𝑞 ⊆ On)
104		ssralv 3629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
106	105	ad2antlr 759	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
107		soseq.4	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ ∅ ∈ 𝐴
108		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑎‘𝑥) = (𝑎‘𝑝))
109		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑏‘𝑥) = (𝑏‘𝑝))
110	108, 109	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑝 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑝) = (𝑏‘𝑝)))
111	110	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝)))
112	111	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝))))
113		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → (𝑏‘𝑝) ∈ 𝐴)
114		fdm 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎:𝑝⟶𝐴 → dom 𝑎 = 𝑝)
115		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑝 ∈ On → Ord 𝑝)
116		ordirr 5658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑝 ∈ On → ¬ 𝑝 ∈ 𝑝)
118		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎 ↔ 𝑝 ∈ 𝑝))
119	118	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝 ∈ 𝑝))
120	119	biimparc 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑝 ∈ 𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121	117, 120	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122		ndmfv 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑝 ∈ dom 𝑎 → (𝑎‘𝑝) = ∅)
123		eqtr2 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ∅ = (𝑏‘𝑝))
124		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∅ = (𝑏‘𝑝) → (∅ ∈ 𝐴 ↔ (𝑏‘𝑝) ∈ 𝐴))
125	124	biimprd 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∅ = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126	123, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127	126	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎‘𝑝) = ∅ → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128	121, 122, 127	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129	128	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
130	114, 129	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ On ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
131	130	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
132	113, 131	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
133	132	exp4b 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))))
134	133	imp32 448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
135	112, 134	syldd 70	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
136	135	com23 84	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴)))
137	136	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴))
138	107, 137	mtoi 189	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑝 ∈ 𝑞)
139	138	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
140	106, 139	syld 46	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
141		onss 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ On → 𝑝 ⊆ On)
142		ssralv 3629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
144	143	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
145		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑎‘𝑥) = (𝑎‘𝑞))
146		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑏‘𝑥) = (𝑏‘𝑞))
147	145, 146	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑞 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑞) = (𝑏‘𝑞)))
148	147	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞)))
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞))))
150		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → (𝑎‘𝑞) ∈ 𝐴)
151		fdm 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏:𝑞⟶𝐴 → dom 𝑏 = 𝑞)
152		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑞 ∈ On → Ord 𝑞)
153		ordirr 5658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
154	152, 153	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑞 ∈ On → ¬ 𝑞 ∈ 𝑞)
155		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏 ↔ 𝑞 ∈ 𝑞))
156	155	notbid 307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞 ∈ 𝑞))
157	156	biimparc 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158		ndmfv 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ 𝑞 ∈ dom 𝑏 → (𝑏‘𝑞) = ∅)
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
160	154, 159	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
161		eqtr 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → (𝑎‘𝑞) = ∅)
162		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163	162	biimpd 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165	164	expcom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) = (𝑏‘𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166	165	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
167	160, 166	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
168	167	adantll 746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
169	151, 168	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
170	150, 169	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
171	170	exp4b 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞⟶𝐴 → (𝑎:𝑝⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
172	171	com23 84	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
173	172	imp32 448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
174	149, 173	syldd 70	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
175	174	com23 84	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴)))
176	175	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴))
177	107, 176	mtoi 189	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑞 ∈ 𝑝)
178	177	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
179	144, 178	syld 46	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
180	140, 179	jcad 554	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝)))
181		ordtri3or 5672	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
182	115, 152, 181	syl2an 493	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
183	182	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
184		3orel13 30853	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝) → ((𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝) → 𝑝 = 𝑞))
185	180, 183, 184	syl6ci 69	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑝 = 𝑞))
186	185, 144	jcad 554	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
187		ffn 5958	. . . . . . . . . . . . . . 15 ⊢ (𝑎:𝑝⟶𝐴 → 𝑎 Fn 𝑝)
188		ffn 5958	. . . . . . . . . . . . . . 15 ⊢ (𝑏:𝑞⟶𝐴 → 𝑏 Fn 𝑞)
189		eqfnfv2 6220	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝑝 ∧ 𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
190	187, 188, 189	syl2an 493	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
191	190	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
192	186, 191	sylibrd 248	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
193	192	ex 449	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)))
194	193	rexlimivv 3018	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
195	102, 194	sylbi 206	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
196	85, 195	syl5 33	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → 𝑎 = 𝑏))
197	75, 196	sylbird 249	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
198	64, 197	syl5bir 232	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
199	53, 198	sylbid 229	. . . . 5 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) → 𝑎 = 𝑏))
200	199	orrd 392	. . . 4 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201		3orcomb 1041	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏))
202		df-3or 1032	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203	201, 202	bitr2i 264	. . . 4 ⊢ (((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
204	200, 203	sylib 207	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
205	204	rgen2a 2960	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)
206		df-so 4960	. 2 ⊢ (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)))
207	6, 205, 206	mpbir2an 957	1 ⊢ 𝑆 Or 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  [wsbc 3402   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583  {copab 4642   Po wpo 4957   Or wor 4958  dom cdm 5038  Ord word 5639  Oncon0 5640   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  sltso  31068