Theorem exmidfodomrlemrALT 7561

Description: The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7560. In particular, this proof uses eldju 7414 instead of djur 7415 and avoids djulclb 7401. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)

Assertion

Ref	Expression
exmidfodomrlemrALT	⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

Distinct variable group:   𝑥,𝑓,𝑦,𝑧

Proof of Theorem exmidfodomrlemrALT

Dummy variables 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1581	. . . . . . . . 9 ⊢ Ⅎ𝑓(∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)
2		nfe1 1549	. . . . . . . . 9 ⊢ Ⅎ𝑓∃𝑓 𝑓:𝑥–onto→𝑦
3	1, 2	nfim 1625	. . . . . . . 8 ⊢ Ⅎ𝑓((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
4	3	nfal 1629	. . . . . . 7 ⊢ Ⅎ𝑓∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
5	4	nfal 1629	. . . . . 6 ⊢ Ⅎ𝑓∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)
6		nfv 1581	. . . . . 6 ⊢ Ⅎ𝑓 𝑢 ⊆ {∅}
7	5, 6	nfan 1618	. . . . 5 ⊢ Ⅎ𝑓(∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅})
8		nfv 1581	. . . . 5 ⊢ Ⅎ𝑓DECID ∅ ∈ 𝑢
9		simpl 109	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
10		p0ex 4327	. . . . . . . . . . . 12 ⊢ {∅} ∈ V
11		ssdomg 7069	. . . . . . . . . . . 12 ⊢ ({∅} ∈ V → (𝑢 ⊆ {∅} → 𝑢 ≼ {∅}))
12	10, 11	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ {∅})
13		df1o2 6705	. . . . . . . . . . 11 ⊢ 1o = {∅}
14	12, 13	breqtrrdi 4173	. . . . . . . . . 10 ⊢ (𝑢 ⊆ {∅} → 𝑢 ≼ 1o)
15		1onn 6797	. . . . . . . . . . 11 ⊢ 1o ∈ ω
16		domrefg 7057	. . . . . . . . . . 11 ⊢ (1o ∈ ω → 1o ≼ 1o)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ 1o ≼ 1o
18		djudom 7439	. . . . . . . . . 10 ⊢ ((𝑢 ≼ 1o ∧ 1o ≼ 1o) → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
19	14, 17, 18	sylancl 417	. . . . . . . . 9 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ (1o ⊔ 1o))
20		dju1p1e2 7555	. . . . . . . . 9 ⊢ (1o ⊔ 1o) ≈ 2o
21		domentr 7082	. . . . . . . . 9 ⊢ (((𝑢 ⊔ 1o) ≼ (1o ⊔ 1o) ∧ (1o ⊔ 1o) ≈ 2o) → (𝑢 ⊔ 1o) ≼ 2o)
22	19, 20, 21	sylancl 417	. . . . . . . 8 ⊢ (𝑢 ⊆ {∅} → (𝑢 ⊔ 1o) ≼ 2o)
23	22	adantl 277	. . . . . . 7 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (𝑢 ⊔ 1o) ≼ 2o)
24		0lt1o 6717	. . . . . . . . 9 ⊢ ∅ ∈ 1o
25		djurcl 7398	. . . . . . . . 9 ⊢ (∅ ∈ 1o → (inr‘∅) ∈ (𝑢 ⊔ 1o))
26	24, 25	ax-mp 5	. . . . . . . 8 ⊢ (inr‘∅) ∈ (𝑢 ⊔ 1o)
27		elex2 2838	. . . . . . . 8 ⊢ ((inr‘∅) ∈ (𝑢 ⊔ 1o) → ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o))
28	26, 27	ax-mp 5	. . . . . . 7 ⊢ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)
29	23, 28	jctil 312	. . . . . 6 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o))
30		vex 2824	. . . . . . . 8 ⊢ 𝑢 ∈ V
31		djuex 7389	. . . . . . . 8 ⊢ ((𝑢 ∈ V ∧ 1o ∈ ω) → (𝑢 ⊔ 1o) ∈ V)
32	30, 15, 31	mp2an 430	. . . . . . 7 ⊢ (𝑢 ⊔ 1o) ∈ V
33		2onn 6798	. . . . . . . 8 ⊢ 2o ∈ ω
34		breq2 4135	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑦 ≼ 𝑥 ↔ 𝑦 ≼ 2o))
35	34	anbi2d 468	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) ↔ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o)))
36		foeq2 5615	. . . . . . . . . . . 12 ⊢ (𝑥 = 2o → (𝑓:𝑥–onto→𝑦 ↔ 𝑓:2o–onto→𝑦))
37	36	exbidv 1878	. . . . . . . . . . 11 ⊢ (𝑥 = 2o → (∃𝑓 𝑓:𝑥–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→𝑦))
38	35, 37	imbi12d 234	. . . . . . . . . 10 ⊢ (𝑥 = 2o → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
39	38	albidv 1877	. . . . . . . . 9 ⊢ (𝑥 = 2o → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ↔ ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
40	39	spcgv 2912	. . . . . . . 8 ⊢ (2o ∈ ω → (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦)))
41	33, 40	ax-mp 5	. . . . . . 7 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦))
42		eleq2 2302	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝑢 ⊔ 1o)))
43	42	exbidv 1878	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑧 𝑧 ∈ 𝑦 ↔ ∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o)))
44		breq1 4134	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑦 ≼ 2o ↔ (𝑢 ⊔ 1o) ≼ 2o))
45	43, 44	anbi12d 477	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) ↔ (∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o)))
46		foeq3 5616	. . . . . . . . . 10 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (𝑓:2o–onto→𝑦 ↔ 𝑓:2o–onto→(𝑢 ⊔ 1o)))
47	46	exbidv 1878	. . . . . . . . 9 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (∃𝑓 𝑓:2o–onto→𝑦 ↔ ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o)))
48	45, 47	imbi12d 234	. . . . . . . 8 ⊢ (𝑦 = (𝑢 ⊔ 1o) → (((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦) ↔ ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))))
49	48	spcgv 2912	. . . . . . 7 ⊢ ((𝑢 ⊔ 1o) ∈ V → (∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 2o) → ∃𝑓 𝑓:2o–onto→𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))))
50	32, 41, 49	mpsyl 65	. . . . . 6 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ((∃𝑧 𝑧 ∈ (𝑢 ⊔ 1o) ∧ (𝑢 ⊔ 1o) ≼ 2o) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o)))
51	9, 29, 50	sylc 62	. . . . 5 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → ∃𝑓 𝑓:2o–onto→(𝑢 ⊔ 1o))
52		simprl 535	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → ∅ ∈ 𝑢)
53	52	orcd 745	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
54		df-dc 847	. . . . . . 7 ⊢ (DECID ∅ ∈ 𝑢 ↔ (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
55	53, 54	sylibr 134	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅))) → DECID ∅ ∈ 𝑢)
56		simprl 535	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅))) → ∅ ∈ 𝑢)
57	56	orcd 745	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅))) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
58	57, 54	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅))) → DECID ∅ ∈ 𝑢)
59		simp-4r 548	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → 𝑓:2o–onto→(𝑢 ⊔ 1o))
60		djulcl 7397	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → (inl‘∅) ∈ (𝑢 ⊔ 1o))
61	60	adantl 277	. . . . . . . . . . . 12 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → (inl‘∅) ∈ (𝑢 ⊔ 1o))
62		foelrn 5961	. . . . . . . . . . . 12 ⊢ ((𝑓:2o–onto→(𝑢 ⊔ 1o) ∧ (inl‘∅) ∈ (𝑢 ⊔ 1o)) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
63	59, 61, 62	syl2anc 415	. . . . . . . . . . 11 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → ∃𝑤 ∈ 2o (inl‘∅) = (𝑓‘𝑤))
64		simprr 537	. . . . . . . . . . . . . . 15 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (inl‘∅) = (𝑓‘𝑤))
65		fvres 5722	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ 𝑢 → ((inl ↾ 𝑢)‘∅) = (inl‘∅))
66	65	eqeq1d 2247	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∈ 𝑢 → (((inl ↾ 𝑢)‘∅) = (𝑓‘𝑤) ↔ (inl‘∅) = (𝑓‘𝑤)))
67	66	ad2antlr 493	. . . . . . . . . . . . . . 15 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (((inl ↾ 𝑢)‘∅) = (𝑓‘𝑤) ↔ (inl‘∅) = (𝑓‘𝑤)))
68	64, 67	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → ((inl ↾ 𝑢)‘∅) = (𝑓‘𝑤))
69	68	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → ((inl ↾ 𝑢)‘∅) = (𝑓‘𝑤))
70		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → 𝑤 = ∅)
71	70	fveq2d 5702	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘𝑤) = (𝑓‘∅))
72		simp-5r 550	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → (𝑓‘∅) = ((inr ↾ 1o)‘∅))
73	69, 71, 72	3eqtrd 2275	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = ∅) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
74	68	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → ((inl ↾ 𝑢)‘∅) = (𝑓‘𝑤))
75		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → 𝑤 = 1o)
76	75	fveq2d 5702	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘𝑤) = (𝑓‘1o))
77		simp-4r 548	. . . . . . . . . . . . 13 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → (𝑓‘1o) = ((inr ↾ 1o)‘∅))
78	74, 76, 77	3eqtrd 2275	. . . . . . . . . . . 12 ⊢ ((((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) ∧ 𝑤 = 1o) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
79		elpri 3732	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {∅, 1o} → (𝑤 = ∅ ∨ 𝑤 = 1o))
80		df2o3 6706	. . . . . . . . . . . . . 14 ⊢ 2o = {∅, 1o}
81	79, 80	eleq2s 2333	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 2o → (𝑤 = ∅ ∨ 𝑤 = 1o))
82	81	ad2antrl 494	. . . . . . . . . . . 12 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → (𝑤 = ∅ ∨ 𝑤 = 1o))
83	73, 78, 82	mpjaodan 810	. . . . . . . . . . 11 ⊢ (((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) ∧ (𝑤 ∈ 2o ∧ (inl‘∅) = (𝑓‘𝑤))) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
84	63, 83	rexlimddv 2673	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
85		0ex 4262	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
86		djune 7424	. . . . . . . . . . . . . 14 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (inl‘∅) ≠ (inr‘∅))
87	85, 85, 86	mp2an 430	. . . . . . . . . . . . 13 ⊢ (inl‘∅) ≠ (inr‘∅)
88	87	neii 2422	. . . . . . . . . . . 12 ⊢ ¬ (inl‘∅) = (inr‘∅)
89		fvres 5722	. . . . . . . . . . . . . . 15 ⊢ (∅ ∈ 1o → ((inr ↾ 1o)‘∅) = (inr‘∅))
90	24, 89	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((inr ↾ 1o)‘∅) = (inr‘∅)
91	90	a1i 9	. . . . . . . . . . . . 13 ⊢ (∅ ∈ 𝑢 → ((inr ↾ 1o)‘∅) = (inr‘∅))
92	65, 91	eqeq12d 2253	. . . . . . . . . . . 12 ⊢ (∅ ∈ 𝑢 → (((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅) ↔ (inl‘∅) = (inr‘∅)))
93	88, 92	mtbiri 686	. . . . . . . . . . 11 ⊢ (∅ ∈ 𝑢 → ¬ ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
94	93	adantl 277	. . . . . . . . . 10 ⊢ ((((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) ∧ ∅ ∈ 𝑢) → ¬ ((inl ↾ 𝑢)‘∅) = ((inr ↾ 1o)‘∅))
95	84, 94	pm2.65da 671	. . . . . . . . 9 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) → ¬ ∅ ∈ 𝑢)
96	95	olcd 746	. . . . . . . 8 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) → (∅ ∈ 𝑢 ∨ ¬ ∅ ∈ 𝑢))
97	96, 54	sylibr 134	. . . . . . 7 ⊢ (((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) ∧ (𝑓‘1o) = ((inr ↾ 1o)‘∅)) → DECID ∅ ∈ 𝑢)
98		simplr 533	. . . . . . . . . 10 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ {∅})
99	98, 13	sseqtrrdi 3297	. . . . . . . . 9 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑢 ⊆ 1o)
100	99	adantr 276	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → 𝑢 ⊆ 1o)
101		fof 5618	. . . . . . . . . . 11 ⊢ (𝑓:2o–onto→(𝑢 ⊔ 1o) → 𝑓:2o⟶(𝑢 ⊔ 1o))
102	101	adantl 277	. . . . . . . . . 10 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
103	102	adantr 276	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → 𝑓:2o⟶(𝑢 ⊔ 1o))
104		1oex 6699	. . . . . . . . . . . 12 ⊢ 1o ∈ V
105	104	prid2 3818	. . . . . . . . . . 11 ⊢ 1o ∈ {∅, 1o}
106	105, 80	eleqtrri 2314	. . . . . . . . . 10 ⊢ 1o ∈ 2o
107	106	a1i 9	. . . . . . . . 9 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → 1o ∈ 2o)
108	103, 107	ffvelcdmd 5847	. . . . . . . 8 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → (𝑓‘1o) ∈ (𝑢 ⊔ 1o))
109	100, 108	exmidfodomrlemreseldju 7558	. . . . . . 7 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → ((∅ ∈ 𝑢 ∧ (𝑓‘1o) = ((inl ↾ 𝑢)‘∅)) ∨ (𝑓‘1o) = ((inr ↾ 1o)‘∅)))
110	58, 97, 109	mpjaodan 810	. . . . . 6 ⊢ ((((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) ∧ (𝑓‘∅) = ((inr ↾ 1o)‘∅)) → DECID ∅ ∈ 𝑢)
111		elelsuc 4556	. . . . . . . . . . 11 ⊢ (∅ ∈ 1o → ∅ ∈ suc 1o)
112	24, 111	ax-mp 5	. . . . . . . . . 10 ⊢ ∅ ∈ suc 1o
113		df-2o 6692	. . . . . . . . . 10 ⊢ 2o = suc 1o
114	112, 113	eleqtrri 2314	. . . . . . . . 9 ⊢ ∅ ∈ 2o
115	114	a1i 9	. . . . . . . 8 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ∅ ∈ 2o)
116	102, 115	ffvelcdmd 5847	. . . . . . 7 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → (𝑓‘∅) ∈ (𝑢 ⊔ 1o))
117	99, 116	exmidfodomrlemreseldju 7558	. . . . . 6 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → ((∅ ∈ 𝑢 ∧ (𝑓‘∅) = ((inl ↾ 𝑢)‘∅)) ∨ (𝑓‘∅) = ((inr ↾ 1o)‘∅)))
118	55, 110, 117	mpjaodan 810	. . . . 5 ⊢ (((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) ∧ 𝑓:2o–onto→(𝑢 ⊔ 1o)) → DECID ∅ ∈ 𝑢)
119	7, 8, 51, 118	exlimdd 1925	. . . 4 ⊢ ((∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) ∧ 𝑢 ⊆ {∅}) → DECID ∅ ∈ 𝑢)
120	119	ex 115	. . 3 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → (𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
121	120	alrimiv 1927	. 2 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
122		df-exmid 4334	. 2 ⊢ (EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → DECID ∅ ∈ 𝑢))
123	121, 122	sylibr 134	1 ⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 720  DECID wdc 846  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209   ≠ wne 2420  ∃wrex 2529  Vcvv 2821   ⊆ wss 3220  ∅c0 3520  {csn 3709  {cpr 3710   class class class wbr 4131  EXMIDwem 4333  suc csuc 4512  ωcom 4739   ↾ cres 4778  ⟶wf 5376  –onto→wfo 5378  ‘cfv 5380  1_oc1o 6684  2_oc2o 6685   ≈ cen 7024   ≼ cdom 7025   ⊔ cdju 7383  inlcinl 7391  inrcinr 7392

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737

This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-exmid 4334  df-id 4440  df-iord 4513  df-on 4515  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-1st 6378  df-2nd 6379  df-1o 6691  df-2o 6692  df-er 6811  df-en 7027  df-dom 7028  df-dju 7384  df-inl 7393  df-inr 7394  df-case 7430

This theorem is used by: (None)