subctctexmid - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > subctctexmid		GIF version

Theorem subctctexmid 14720

Description: If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.)

**Hypotheses**
Ref	Expression
subctctexmid.x	⊢ (𝜑 → ∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_o)))
subctctexmid.mk	⊢ (𝜑 → ω ∈ Markov)

**Assertion**
Ref	Expression
subctctexmid	⊢ (𝜑 → EXMID)

Distinct variable groups: 𝑓,𝑠,𝑥 𝜑,𝑔 𝑥,𝑔 Allowed substitution hints: 𝜑(𝑥,𝑓,𝑠)

Proof of Theorem subctctexmid Dummy variables 𝑦 𝑧 ℎ 𝑛 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		subctctexmid.x	. . . . 5 ⊢ (𝜑 → ∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_o)))
2		omex 4592	. . . . . . . 8 ⊢ ω ∈ V
3	2	rabex 4147	. . . . . . 7 ⊢ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V
4	3	a1i 9	. . . . . 6 ⊢ (𝜑 → {𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V)
5		ssrab2 3240	. . . . . . 7 ⊢ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω
6		f1oi 5499	. . . . . . . . 9 ⊢ ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–1-1-onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
7		f1ofo 5468	. . . . . . . . 9 ⊢ (( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–1-1-onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} → ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
8	6, 7	ax-mp 5	. . . . . . . 8 ⊢ ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
9		resiexg 4952	. . . . . . . . . 10 ⊢ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V → ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) ∈ V)
10	3, 9	ax-mp 5	. . . . . . . . 9 ⊢ ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) ∈ V
11		foeq1 5434	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}) → (𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
12	10, 11	spcev 2832	. . . . . . . 8 ⊢ (( I ↾ {𝑧 ∈ ω ∣ 𝑦 = {∅}}):{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} → ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
13	8, 12	ax-mp 5	. . . . . . 7 ⊢ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}
14	5, 13	pm3.2i 272	. . . . . 6 ⊢ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})
15		sseq1 3178	. . . . . . . 8 ⊢ (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑠 ⊆ ω ↔ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω))
16		foeq2 5435	. . . . . . . . 9 ⊢ (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
17	16	exbidv 1825	. . . . . . . 8 ⊢ (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
18	15, 17	anbi12d 473	. . . . . . 7 ⊢ (𝑠 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) ↔ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
19	18	spcegv 2825	. . . . . 6 ⊢ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ∈ V → (({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊆ ω ∧ ∃𝑓 𝑓:{𝑧 ∈ ω ∣ 𝑦 = {∅}}–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
20	4, 14, 19	mpisyl 1446	. . . . 5 ⊢ (𝜑 → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
21		foeq3 5436	. . . . . . . . . 10 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑓:𝑠–onto→𝑥 ↔ 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
22	21	exbidv 1825	. . . . . . . . 9 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑓 𝑓:𝑠–onto→𝑥 ↔ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}))
23	22	anbi2d 464	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) ↔ (𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
24	23	exbidv 1825	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) ↔ ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}})))
25		djueq1 7038	. . . . . . . . 9 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑥 ⊔ 1_o) = ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
26		foeq3 5436	. . . . . . . . 9 ⊢ ((𝑥 ⊔ 1_o) = ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o) → (𝑔:ω–onto→(𝑥 ⊔ 1_o) ↔ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)))
27	25, 26	syl 14	. . . . . . . 8 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (𝑔:ω–onto→(𝑥 ⊔ 1_o) ↔ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)))
28	27	exbidv 1825	. . . . . . 7 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_o) ↔ ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)))
29	24, 28	imbi12d 234	. . . . . 6 ⊢ (𝑥 = {𝑧 ∈ ω ∣ 𝑦 = {∅}} → ((∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_o)) ↔ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))))
30	3, 29	spcv 2831	. . . . 5 ⊢ (∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_o)) → (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→{𝑧 ∈ ω ∣ 𝑦 = {∅}}) → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)))
31	1, 20, 30	sylc 62	. . . 4 ⊢ (𝜑 → ∃𝑔 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
32		fveq1 5514	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) → (ℎ‘𝑛) = ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛))
33	32	eqeq1d 2186	. . . . . . . . . . 11 ⊢ (ℎ = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) → ((ℎ‘𝑛) = 1_o ↔ ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
34	33	rexbidv 2478	. . . . . . . . . 10 ⊢ (ℎ = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) → (∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o ↔ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
35	34	notbid 667	. . . . . . . . 9 ⊢ (ℎ = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) → (¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o ↔ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
36	35	notbid 667	. . . . . . . 8 ⊢ (ℎ = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) → (¬ ¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o ↔ ¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
37	36, 34	imbi12d 234	. . . . . . 7 ⊢ (ℎ = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) → ((¬ ¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o → ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o) ↔ (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o)))
38		subctctexmid.mk	. . . . . . . . 9 ⊢ (𝜑 → ω ∈ Markov)
39		ismkvnex 7152	. . . . . . . . . 10 ⊢ (ω ∈ Markov → (ω ∈ Markov ↔ ∀ℎ ∈ (2_o ↑_𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o → ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o)))
40	38, 39	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (ω ∈ Markov ↔ ∀ℎ ∈ (2_o ↑_𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o → ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o)))
41	38, 40	mpbid 147	. . . . . . . 8 ⊢ (𝜑 → ∀ℎ ∈ (2_o ↑_𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o → ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o))
42	41	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → ∀ℎ ∈ (2_o ↑_𝑚 ω)(¬ ¬ ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o → ∃𝑛 ∈ ω (ℎ‘𝑛) = 1_o))
43		1lt2o 6442	. . . . . . . . . . . 12 ⊢ 1_o ∈ 2_o
44	43	a1i 9	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ (1^st ‘(𝑔‘𝑛)) = ∅) → 1_o ∈ 2_o)
45		0lt2o 6441	. . . . . . . . . . . 12 ⊢ ∅ ∈ 2_o
46	45	a1i 9	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ ¬ (1^st ‘(𝑔‘𝑛)) = ∅) → ∅ ∈ 2_o)
47		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
48		fof 5438	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o) → 𝑔:ω⟶({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
49	47, 48	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → 𝑔:ω⟶({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
50		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
51	49, 50	ffvelcdmd 5652	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → (𝑔‘𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
52		eldju1st 7069	. . . . . . . . . . . . 13 ⊢ ((𝑔‘𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o) → ((1^st ‘(𝑔‘𝑛)) = ∅ ∨ (1^st ‘(𝑔‘𝑛)) = 1_o))
53	51, 52	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → ((1^st ‘(𝑔‘𝑛)) = ∅ ∨ (1^st ‘(𝑔‘𝑛)) = 1_o))
54		1n0 6432	. . . . . . . . . . . . . . . 16 ⊢ 1_o ≠ ∅
55	54	neii 2349	. . . . . . . . . . . . . . 15 ⊢ ¬ 1_o = ∅
56		eqeq1 2184	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘(𝑔‘𝑛)) = 1_o → ((1^st ‘(𝑔‘𝑛)) = ∅ ↔ 1_o = ∅))
57	55, 56	mtbiri 675	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘(𝑔‘𝑛)) = 1_o → ¬ (1^st ‘(𝑔‘𝑛)) = ∅)
58	57	orim2i 761	. . . . . . . . . . . . 13 ⊢ (((1^st ‘(𝑔‘𝑛)) = ∅ ∨ (1^st ‘(𝑔‘𝑛)) = 1_o) → ((1^st ‘(𝑔‘𝑛)) = ∅ ∨ ¬ (1^st ‘(𝑔‘𝑛)) = ∅))
59		df-dc 835	. . . . . . . . . . . . 13 ⊢ (DECID (1^st ‘(𝑔‘𝑛)) = ∅ ↔ ((1^st ‘(𝑔‘𝑛)) = ∅ ∨ ¬ (1^st ‘(𝑔‘𝑛)) = ∅))
60	58, 59	sylibr 134	. . . . . . . . . . . 12 ⊢ (((1^st ‘(𝑔‘𝑛)) = ∅ ∨ (1^st ‘(𝑔‘𝑛)) = 1_o) → DECID (1^st ‘(𝑔‘𝑛)) = ∅)
61	53, 60	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → DECID (1^st ‘(𝑔‘𝑛)) = ∅)
62	44, 46, 61	ifcldadc 3563	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) ∈ 2_o)
63	62	fmpttd 5671	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (𝑛 ∈ ω ↦ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅)):ω⟶2_o)
64		2fveq3 5520	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑛 → (1^st ‘(𝑔‘𝑤)) = (1^st ‘(𝑔‘𝑛)))
65	64	eqeq1d 2186	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑛 → ((1^st ‘(𝑔‘𝑤)) = ∅ ↔ (1^st ‘(𝑔‘𝑛)) = ∅))
66	65	ifbid 3555	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑛 → if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅) = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅))
67		eqcom 2179	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑛 ↔ 𝑛 = 𝑤)
68		eqcom 2179	. . . . . . . . . . . 12 ⊢ (if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅) = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) ↔ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))
69	66, 67, 68	3imtr3i 200	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑤 → if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))
70	69	cbvmptv 4099	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω ↦ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅)) = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))
71	70	feq1i 5358	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ↦ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅)):ω⟶2_o ↔ (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)):ω⟶2_o)
72	63, 71	sylib 122	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)):ω⟶2_o)
73		2onn 6521	. . . . . . . . . 10 ⊢ 2_o ∈ ω
74	73	elexi 2749	. . . . . . . . 9 ⊢ 2_o ∈ V
75	74, 2	elmap 6676	. . . . . . . 8 ⊢ ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) ∈ (2_o ↑_𝑚 ω) ↔ (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)):ω⟶2_o)
76	72, 75	sylibr 134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) ∈ (2_o ↑_𝑚 ω))
77	37, 42, 76	rspcdva 2846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
78		eqid 2177	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅)) = (𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))
79	78, 66, 50, 62	fvmptd3 5609	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅))
80	79	eqeq1d 2186	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → (((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o ↔ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o))
81	51	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → (𝑔‘𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
82		simpr 110	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o)
83	82	eqcomd 2183	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → 1_o = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅))
84		eqifdc 3569	. . . . . . . . . . . . . . . . . . 19 ⊢ (DECID (1^st ‘(𝑔‘𝑛)) = ∅ → (1_o = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) ↔ (((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ∨ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅))))
85	61, 84	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → (1_o = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) ↔ (((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ∨ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅))))
86		eqid 2177	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_o = 1_o
87		orcom 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ∨ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅)) ↔ ((¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅) ∨ ((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o)))
88	55	intnan 929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅)
89		biorf 744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅) → (((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ↔ ((¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅) ∨ ((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o))))
90	88, 89	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ↔ ((¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅) ∨ ((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o)))
91	87, 90	bitr4i 187	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ∨ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅)) ↔ ((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o))
92	86, 91	mpbiran2 941	. . . . . . . . . . . . . . . . . 18 ⊢ ((((1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = 1_o) ∨ (¬ (1^st ‘(𝑔‘𝑛)) = ∅ ∧ 1_o = ∅)) ↔ (1^st ‘(𝑔‘𝑛)) = ∅)
93	85, 92	bitrdi 196	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → (1_o = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) ↔ (1^st ‘(𝑔‘𝑛)) = ∅))
94	93	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → (1_o = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) ↔ (1^st ‘(𝑔‘𝑛)) = ∅))
95	83, 94	mpbid 147	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → (1^st ‘(𝑔‘𝑛)) = ∅)
96		eldju2ndl 7070	. . . . . . . . . . . . . . 15 ⊢ (((𝑔‘𝑛) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o) ∧ (1^st ‘(𝑔‘𝑛)) = ∅) → (2^nd ‘(𝑔‘𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
97	81, 95, 96	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → (2^nd ‘(𝑔‘𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
98		biidd 172	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (2^nd ‘(𝑔‘𝑛)) → (𝑦 = {∅} ↔ 𝑦 = {∅}))
99	98	elrab 2893	. . . . . . . . . . . . . 14 ⊢ ((2^nd ‘(𝑔‘𝑛)) ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}} ↔ ((2^nd ‘(𝑔‘𝑛)) ∈ ω ∧ 𝑦 = {∅}))
100	97, 99	sylib 122	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → ((2^nd ‘(𝑔‘𝑛)) ∈ ω ∧ 𝑦 = {∅}))
101	100	simprd 114	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) ∧ if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o) → 𝑦 = {∅})
102	101	ex 115	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → (if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o → 𝑦 = {∅}))
103	80, 102	sylbid 150	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑛 ∈ ω) → (((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o → 𝑦 = {∅}))
104	103	rexlimdva 2594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o → 𝑦 = {∅}))
105		simplr 528	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
106		biidd 172	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ∅ → (𝑦 = {∅} ↔ 𝑦 = {∅}))
107		peano1 4593	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ ω
108	107	a1i 9	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → ∅ ∈ ω)
109		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → 𝑦 = {∅})
110	106, 108, 109	elrabd 2895	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → ∅ ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}})
111		djulcl 7049	. . . . . . . . . . . . 13 ⊢ (∅ ∈ {𝑧 ∈ ω ∣ 𝑦 = {∅}} → (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
112	110, 111	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o))
113		foelrn 5753	. . . . . . . . . . . 12 ⊢ ((𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o) ∧ (inl‘∅) ∈ ({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → ∃𝑛 ∈ ω (inl‘∅) = (𝑔‘𝑛))
114	105, 112, 113	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → ∃𝑛 ∈ ω (inl‘∅) = (𝑔‘𝑛))
115	79	adantlr 477	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) → ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅))
116		fveq2 5515	. . . . . . . . . . . . . . . 16 ⊢ ((inl‘∅) = (𝑔‘𝑛) → (1^st ‘(inl‘∅)) = (1^st ‘(𝑔‘𝑛)))
117		1stinl 7072	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ∈ ω → (1^st ‘(inl‘∅)) = ∅)
118	107, 117	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘(inl‘∅)) = ∅
119	116, 118	eqtr3di 2225	. . . . . . . . . . . . . . 15 ⊢ ((inl‘∅) = (𝑔‘𝑛) → (1^st ‘(𝑔‘𝑛)) = ∅)
120	119	iftrued 3541	. . . . . . . . . . . . . 14 ⊢ ((inl‘∅) = (𝑔‘𝑛) → if((1^st ‘(𝑔‘𝑛)) = ∅, 1_o, ∅) = 1_o)
121	115, 120	sylan9eq 2230	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) ∧ (inl‘∅) = (𝑔‘𝑛)) → ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o)
122	121	ex 115	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) ∧ 𝑛 ∈ ω) → ((inl‘∅) = (𝑔‘𝑛) → ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
123	122	reximdva 2579	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → (∃𝑛 ∈ ω (inl‘∅) = (𝑔‘𝑛) → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
124	114, 123	mpd 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) ∧ 𝑦 = {∅}) → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o)
125	124	ex 115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (𝑦 = {∅} → ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o))
126	104, 125	impbid 129	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o ↔ 𝑦 = {∅}))
127	126	notbid 667	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o ↔ ¬ 𝑦 = {∅}))
128	127	notbid 667	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (¬ ¬ ∃𝑛 ∈ ω ((𝑤 ∈ ω ↦ if((1^st ‘(𝑔‘𝑤)) = ∅, 1_o, ∅))‘𝑛) = 1_o ↔ ¬ ¬ 𝑦 = {∅}))
129	77, 128, 126	3imtr3d 202	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → (¬ ¬ 𝑦 = {∅} → 𝑦 = {∅}))
130		df-stab 831	. . . . 5 ⊢ (STAB 𝑦 = {∅} ↔ (¬ ¬ 𝑦 = {∅} → 𝑦 = {∅}))
131	129, 130	sylibr 134	. . . 4 ⊢ ((𝜑 ∧ 𝑔:ω–onto→({𝑧 ∈ ω ∣ 𝑦 = {∅}} ⊔ 1_o)) → STAB 𝑦 = {∅})
132	31, 131	exlimddv 1898	. . 3 ⊢ (𝜑 → STAB 𝑦 = {∅})
133	132	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝑦 ⊆ {∅}) → STAB 𝑦 = {∅})
134	133	exmid1stab 4208	1 ⊢ (𝜑 → EXMID)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 STAB wstab 830 DECID wdc 834 ∀wal 1351 = wceq 1353 ∃wex 1492 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 {crab 2459 Vcvv 2737 ⊆ wss 3129 ∅c0 3422 ifcif 3534 {csn 3592 ↦ cmpt 4064 EXMIDwem 4194 I cid 4288 ωcom 4589 ↾ cres 4628 ⟶wf 5212 –onto→wfo 5214 –1-1-onto→wf1o 5215 ‘cfv 5216 (class class class)co 5874 1^st c1st 6138 2^nd c2nd 6139 1_oc1o 6409 2_oc2o 6410 ↑_𝑚 cmap 6647 ⊔ cdju 7035 inlcinl 7043 Markovcmarkov 7148

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-nul 4129 ax-pow 4174 ax-pr 4209 ax-un 4433 ax-setind 4536 ax-iinf 4587

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-int 3845 df-br 4004 df-opab 4065 df-mpt 4066 df-tr 4102 df-exmid 4195 df-id 4293 df-iord 4366 df-on 4368 df-suc 4371 df-iom 4590 df-xp 4632 df-rel 4633 df-cnv 4634 df-co 4635 df-dm 4636 df-rn 4637 df-res 4638 df-ima 4639 df-iota 5178 df-fun 5218 df-fn 5219 df-f 5220 df-f1 5221 df-fo 5222 df-f1o 5223 df-fv 5224 df-ov 5877 df-oprab 5878 df-mpo 5879 df-1st 6140 df-2nd 6141 df-1o 6416 df-2o 6417 df-map 6649 df-dju 7036 df-inl 7045 df-inr 7046 df-markov 7149

This theorem is referenced by: (None)

W3C validator