Theorem soseq 33209

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 5456	. . . 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 33208	. 2 ⊢ 𝑆 Po 𝐹
7		eleq1w 2872	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
8	7	anbi1d 632	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
9		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦))
10	9	eqeq1d 2800	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦)))
11	10	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦)))
12		fveq1 6644	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥))
13	12	breq1d 5040	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))
14	11, 13	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
15	14	rexbidv 3256	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))
16	8, 15	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))))
17		eleq1w 2872	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
18	17	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹)))
19		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦))
20	19	eqeq2d 2809	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
21	20	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦)))
22		fveq1 6644	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑏 → (𝑔‘𝑥) = (𝑏‘𝑥))
23	22	breq2d 5042	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑏 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))
24	21, 23	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
25	24	rexbidv 3256	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
26	18, 25	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
27	16, 26, 5	brabg 5391	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))))
28	27	bianabs 545	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))
29		eleq1w 2872	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹))
30	29	anbi1d 632	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹)))
31		fveq1 6644	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦))
32	31	eqeq1d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦)))
33	32	ralbidv 3162	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦)))
34		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓‘𝑥) = (𝑏‘𝑥))
35	34	breq1d 5040	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))
36	33, 35	anbi12d 633	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
37	36	rexbidv 3256	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))
38	30, 37	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))))
39		eleq1w 2872	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹))
40	39	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹)))
41		fveq1 6644	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦))
42	41	eqeq2d 2809	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦)))
43	42	ralbidv 3162	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦)))
44		fveq1 6644	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥))
45	44	breq2d 5042	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑎 → ((𝑏‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
46	43, 45	anbi12d 633	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
47	46	rexbidv 3256	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
48	40, 47	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑎 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
49	38, 48, 5	brabg 5391	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
50	49	bianabs 545	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
51	50	ancoms 462	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
52	28, 51	orbi12d 916	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
53	52	notbid 321	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
54		ralinexa 3223	. . . . . . . 8 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
55		andi 1005	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
56		eqcom 2805	. . . . . . . . . . . . . 14 ⊢ ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦))
57	56	ralbii 3133	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦))
58	57	anbi1i 626	. . . . . . . . . . . 12 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))
59	58	orbi2i 910	. . . . . . . . . . 11 ⊢ (((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
60	55, 59	bitri 278	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
61	60	rexbii 3210	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
62		r19.43 3304	. . . . . . . . 9 ⊢ (∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
63	61, 62	bitri 278	. . . . . . . 8 ⊢ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
64	54, 63	xchbinx 337	. . . . . . 7 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
65		feq2 6469	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑦⟶𝐴))
66	65	cbvrexvw 3397	. . . . . . . . . . . . . 14 ⊢ (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴)
67	66	abbii 2863	. . . . . . . . . . . . 13 ⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
68	4, 67	eqtri 2821	. . . . . . . . . . . 12 ⊢ 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴}
69	68	orderseqlem 33207	. . . . . . . . . . 11 ⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅}))
70	68	orderseqlem 33207	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))
71		sotrieq 5466	. . . . . . . . . . . 12 ⊢ ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
72	1, 71	mpan 689	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
73	69, 70, 72	syl2an 598	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))
74	73	imbi2d 344	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
75	74	ralbidv 3162	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))))
76		vex 3444	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
77		fveq2 6645	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑎‘𝑥) = (𝑎‘𝑦))
78		fveq2 6645	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑏‘𝑥) = (𝑏‘𝑦))
79	77, 78	eqeq12d 2814	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)))
80	76, 79	sbcie 3760	. . . . . . . . . . . . 13 ⊢ ([𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦))
81	80	ralbii 3133	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦))
82	81	imbi1i 353	. . . . . . . . . . 11 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
83	82	ralbii 3133	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)))
84		tfisg 33168	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
85	83, 84	sylbir 238	. . . . . . . . 9 ⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥))
86		vex 3444	. . . . . . . . . . . . . 14 ⊢ 𝑎 ∈ V
87		feq1 6468	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑎 → (𝑓:𝑥⟶𝐴 ↔ 𝑎:𝑥⟶𝐴))
88	87	rexbidv 3256	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴))
89	86, 88, 4	elab2 3618	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴)
90		feq2 6469	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑝 → (𝑎:𝑥⟶𝐴 ↔ 𝑎:𝑝⟶𝐴))
91	90	cbvrexvw 3397	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑎:𝑥⟶𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
92	89, 91	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴)
93		vex 3444	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
94		feq1 6468	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑏:𝑥⟶𝐴))
95	94	rexbidv 3256	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴))
96	93, 95, 4	elab2 3618	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴)
97		feq2 6469	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (𝑏:𝑥⟶𝐴 ↔ 𝑏:𝑞⟶𝐴))
98	97	cbvrexvw 3397	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ On 𝑏:𝑥⟶𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
99	96, 98	bitri 278	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)
100	92, 99	anbi12i 629	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
101		reeanv 3320	. . . . . . . . . . 11 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴))
102	100, 101	bitr4i 281	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴))
103		onss 7485	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ On → 𝑞 ⊆ On)
104		ssralv 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
106	105	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)))
107		soseq.4	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ ∅ ∈ 𝐴
108		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑎‘𝑥) = (𝑎‘𝑝))
109		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑝 → (𝑏‘𝑥) = (𝑏‘𝑝))
110	108, 109	eqeq12d 2814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑝 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑝) = (𝑏‘𝑝)))
111	110	rspcv 3566	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝)))
112	111	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝))))
113		ffvelrn 6826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → (𝑏‘𝑝) ∈ 𝐴)
114		fdm 6495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎:𝑝⟶𝐴 → dom 𝑎 = 𝑝)
115		eloni 6169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑝 ∈ On → Ord 𝑝)
116		ordirr 6177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑝 ∈ On → ¬ 𝑝 ∈ 𝑝)
118		eleq2 2878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎 ↔ 𝑝 ∈ 𝑝))
119	118	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (dom 𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝 ∈ 𝑝))
120	119	biimparc 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑝 ∈ 𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
121	117, 120	sylan 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎)
122		ndmfv 6675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑝 ∈ dom 𝑎 → (𝑎‘𝑝) = ∅)
123		eqtr2 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ∅ = (𝑏‘𝑝))
124		eleq1 2877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∅ = (𝑏‘𝑝) → (∅ ∈ 𝐴 ↔ (𝑏‘𝑝) ∈ 𝐴))
125	124	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∅ = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
126	123, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))
127	126	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎‘𝑝) = ∅ → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
128	121, 122, 127	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)))
129	128	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
130	114, 129	sylan2 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ On ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
131	130	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
132	113, 131	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
133	132	exp4b 434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))))
134	133	imp32 422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴)))
135	112, 134	syldd 72	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
136	135	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴)))
137	136	imp 410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴))
138	107, 137	mtoi 202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑝 ∈ 𝑞)
139	138	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
140	106, 139	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞))
141		onss 7485	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ On → 𝑝 ⊆ On)
142		ssralv 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ⊆ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
144	143	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))
145		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑎‘𝑥) = (𝑎‘𝑞))
146		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑞 → (𝑏‘𝑥) = (𝑏‘𝑞))
147	145, 146	eqeq12d 2814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑞 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑞) = (𝑏‘𝑞)))
148	147	rspcv 3566	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞)))
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞))))
150		ffvelrn 6826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → (𝑎‘𝑞) ∈ 𝐴)
151		fdm 6495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏:𝑞⟶𝐴 → dom 𝑏 = 𝑞)
152		eloni 6169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑞 ∈ On → Ord 𝑞)
153		ordirr 6177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
154	152, 153	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑞 ∈ On → ¬ 𝑞 ∈ 𝑞)
155		eleq2 2878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (dom 𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏 ↔ 𝑞 ∈ 𝑞))
156	155	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (dom 𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞 ∈ 𝑞))
157	156	biimparc 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏)
158		ndmfv 6675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (¬ 𝑞 ∈ dom 𝑏 → (𝑏‘𝑞) = ∅)
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((¬ 𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
160	154, 159	sylan 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅)
161		eqtr 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → (𝑎‘𝑞) = ∅)
162		eleq1 2877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴))
163	162	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))
165	164	expcom 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) = (𝑏‘𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)))
166	165	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
167	160, 166	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
168	167	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
169	151, 168	sylan2 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
170	150, 169	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
171	170	exp4b 434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞⟶𝐴 → (𝑎:𝑝⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
172	171	com23 86	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))))
173	172	imp32 422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴)))
174	149, 173	syldd 72	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴)))
175	174	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴)))
176	175	imp 410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴))
177	107, 176	mtoi 202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑞 ∈ 𝑝)
178	177	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
179	144, 178	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝))
180	140, 179	jcad 516	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝)))
181		ordtri3or 6191	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord 𝑝 ∧ Ord 𝑞) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
182	115, 152, 181	syl2an 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
183	182	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝))
184		3orel13 33060	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝) → ((𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝) → 𝑝 = 𝑞))
185	180, 183, 184	syl6ci 71	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑝 = 𝑞))
186	185, 144	jcad 516	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
187		ffn 6487	. . . . . . . . . . . . . . 15 ⊢ (𝑎:𝑝⟶𝐴 → 𝑎 Fn 𝑝)
188		ffn 6487	. . . . . . . . . . . . . . 15 ⊢ (𝑏:𝑞⟶𝐴 → 𝑏 Fn 𝑞)
189		eqfnfv2 6780	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝑝 ∧ 𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
190	187, 188, 189	syl2an 598	. . . . . . . . . . . . . 14 ⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
191	190	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))))
192	186, 191	sylibrd 262	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
193	192	ex 416	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)))
194	193	rexlimivv 3251	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
195	102, 194	sylbi 220	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))
196	85, 195	syl5 34	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → 𝑎 = 𝑏))
197	75, 196	sylbird 263	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
198	64, 197	syl5bir 246	. . . . . 6 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏))
199	53, 198	sylbid 243	. . . . 5 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) → 𝑎 = 𝑏))
200	199	orrd 860	. . . 4 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
201		3orcomb 1091	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏))
202		df-3or 1085	. . . . 5 ⊢ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏))
203	201, 202	bitr2i 279	. . . 4 ⊢ (((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
204	200, 203	sylib 221	. . 3 ⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))
205	204	rgen2 3168	. 2 ⊢ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)
206		df-so 5439	. 2 ⊢ (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)))
207	6, 205, 206	mpbir2an 710	1 ⊢ 𝑆 Or 𝐹

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  [wsbc 3720   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  {csn 4525   class class class wbr 5030  {copab 5092   Po wpo 5436   Or wor 5437  dom cdm 5519  Ord word 6158  Oncon0 6159   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6162  df-on 6163  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332

This theorem is referenced by:  sltso  33294