zfz1isolem1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > zfz1isolem1		GIF version

Theorem zfz1isolem1 10775

Description: Lemma for zfz1iso 10776. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)

**Hypotheses**
Ref	Expression
zfz1isolem1.k	⊢ (𝜑 → 𝐾 ∈ ω)
zfz1isolem1.h	⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))
zfz1isolem1.xz	⊢ (𝜑 → 𝑋 ⊆ ℤ)
zfz1isolem1.xf	⊢ (𝜑 → 𝑋 ∈ Fin)
zfz1isolem1.xs	⊢ (𝜑 → 𝑋 ≈ suc 𝐾)
zfz1isolem1.mx	⊢ (𝜑 → 𝑀 ∈ 𝑋)
zfz1isolem1.m	⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)

**Assertion**
Ref	Expression
zfz1isolem1	⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Distinct variable groups: 𝑦,𝐾 𝑧,𝑀 𝑓,𝑀,𝑦 𝑧,𝑋 𝑓,𝑋,𝑦 Allowed substitution hints: 𝜑(𝑦,𝑧,𝑓) 𝐾(𝑧,𝑓)

Proof of Theorem zfz1isolem1 Dummy variables 𝑎 𝑏 𝑔 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfz1isolem1.xz	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ ℤ)
2	1	ssdifssd 3265	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ⊆ ℤ)
3		zfz1isolem1.xf	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
4		zfz1isolem1.mx	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ 𝑋)
5		diffisn 6871	. . . . . 6 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin)
6	3, 4, 5	syl2anc 409	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin)
7		zfz1isolem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ω)
8		zfz1isolem1.xs	. . . . . 6 ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)
9		dif1en 6857	. . . . . 6 ⊢ ((𝐾 ∈ ω ∧ 𝑋 ≈ suc 𝐾 ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ≈ 𝐾)
10	7, 8, 4, 9	syl3anc 1233	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ≈ 𝐾)
11	2, 6, 10	jca31 307	. . . 4 ⊢ (𝜑 → (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾))
12		zfz1isolem1.h	. . . . 5 ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))
13		sseq1 3170	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ⊆ ℤ ↔ (𝑋 ∖ {𝑀}) ⊆ ℤ))
14		eleq1 2233	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ∈ Fin ↔ (𝑋 ∖ {𝑀}) ∈ Fin))
15	13, 14	anbi12d 470	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ↔ ((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin)))
16		breq1 3992	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾))
17	15, 16	anbi12d 470	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)))
18		fveq2 5496	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀})))
19	18	oveq2d 5869	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))))
20		isoeq4 5783	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
21	19, 20	syl 14	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
22		isoeq5 5784	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
23	21, 22	bitrd 187	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
24	23	exbidv 1818	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
25	17, 24	imbi12d 233	. . . . . . 7 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) ↔ ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))))
26	25	spcgv 2817	. . . . . 6 ⊢ ((𝑋 ∖ {𝑀}) ∈ Fin → (∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) → ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))))
27	6, 26	syl 14	. . . . 5 ⊢ (𝜑 → (∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) → ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))))
28	12, 27	mpd 13	. . . 4 ⊢ (𝜑 → ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
29	11, 28	mpd 13	. . 3 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
30		isoeq1 5780	. . . 4 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
31	30	cbvexv 1911	. . 3 ⊢ (∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
32	29, 31	sylib 121	. 2 ⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
33		df-isom 5207	. . . . . . . . 9 ⊢ (𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣))))
34	33	biimpi 119	. . . . . . . 8 ⊢ (𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) → (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣))))
35	34	adantl 275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣))))
36	35	simpld 111	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}))
37		hashcl 10715	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ₀)
38	3, 37	syl 14	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ₀)
39	38	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (♯‘𝑋) ∈ ℕ₀)
40	4	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑀 ∈ 𝑋)
41		f1osng 5483	. . . . . . 7 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
42	39, 40, 41	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
43		hashdifsn 10754	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
44	3, 4, 43	syl2anc 409	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
45	44	oveq1d 5868	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) + 1))
46	38	nn0cnd 9190	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
47		1cnd 7936	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
48	46, 47	npcand 8234	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
49	45, 48	eqtrd 2203	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋))
50	49	sneqd 3596	. . . . . . . . 9 ⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)})
51	50	ineq2d 3328	. . . . . . . 8 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}))
52		fzp1disj 10036	. . . . . . . 8 ⊢ ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅
53	51, 52	eqtr3di 2218	. . . . . . 7 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
54	53	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
55		incom 3319	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀}))
56		disjdif 3487	. . . . . . . 8 ⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅
57	55, 56	eqtri 2191	. . . . . . 7 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅
58	57	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)
59		f1oun 5462	. . . . . 6 ⊢ (((𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀}) ∧ (((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅ ∧ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
60	36, 42, 54, 58, 59	syl22anc 1234	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
61	3, 4	zfz1isolemsplit 10773	. . . . . . 7 ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))
62		fidifsnid 6849	. . . . . . . . 9 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
63	3, 4, 62	syl2anc 409	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
64	63	eqcomd 2176	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀}))
65		f1oeq23 5434	. . . . . . 7 ⊢ (((1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}) ∧ 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀})) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
66	61, 64, 65	syl2anc 409	. . . . . 6 ⊢ (𝜑 → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
67	66	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
68	60, 67	mpbird 166	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋)
69	3	ad2antrr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ∈ Fin)
70	1	ad2antrr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ⊆ ℤ)
71	4	ad2antrr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑀 ∈ 𝑋)
72		zfz1isolem1.m	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
73	72	ad2antrr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
74		simplr 525	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
75		simprl 526	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑎 ∈ (1...(♯‘𝑋)))
76		simprr 527	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑏 ∈ (1...(♯‘𝑋)))
77	69, 70, 71, 73, 74, 75, 76	zfz1isolemiso 10774	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
78	77	ralrimivva 2552	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
79		df-isom 5207	. . . 4 ⊢ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ∧ ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏))))
80	68, 78, 79	sylanbrc 415	. . 3 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋))
81		vex 2733	. . . . . . 7 ⊢ 𝑔 ∈ V
82	81	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝑔 ∈ V)
83		opexg 4213	. . . . . . . 8 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
84	38, 4, 83	syl2anc 409	. . . . . . 7 ⊢ (𝜑 → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
85		snexg 4170	. . . . . . 7 ⊢ (⟨(♯‘𝑋), 𝑀⟩ ∈ V → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
86	84, 85	syl 14	. . . . . 6 ⊢ (𝜑 → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
87		unexg 4428	. . . . . 6 ⊢ ((𝑔 ∈ V ∧ {⟨(♯‘𝑋), 𝑀⟩} ∈ V) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
88	82, 86, 87	syl2anc 409	. . . . 5 ⊢ (𝜑 → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
89		isoeq1 5780	. . . . . 6 ⊢ (𝑓 = (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) → (𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋)))
90	89	spcegv 2818	. . . . 5 ⊢ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)))
91	88, 90	syl 14	. . . 4 ⊢ (𝜑 → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)))
92	91	adantr 274	. . 3 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)))
93	80, 92	mpd 13	. 2 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))
94	32, 93	exlimddv 1891	1 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1346 = wceq 1348 ∃wex 1485 ∈ wcel 2141 ∀wral 2448 Vcvv 2730 ∖ cdif 3118 ∪ cun 3119 ∩ cin 3120 ⊆ wss 3121 ∅c0 3414 {csn 3583 ⟨cop 3586 class class class wbr 3989 suc csuc 4350 ωcom 4574 –1-1-onto→wf1o 5197 ‘cfv 5198 Isom wiso 5199 (class class class)co 5853 ≈ cen 6716 Fincfn 6718 1c1 7775 + caddc 7777 < clt 7954 ≤ cle 7955 − cmin 8090 ℕ₀cn0 9135 ℤcz 9212 ...cfz 9965 ♯chash 10709

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-addcom 7874 ax-addass 7876 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-0id 7882 ax-rnegex 7883 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-irdg 6349 df-frec 6370 df-1o 6395 df-oadd 6399 df-er 6513 df-en 6719 df-dom 6720 df-fin 6721 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-inn 8879 df-n0 9136 df-z 9213 df-uz 9488 df-fz 9966 df-ihash 10710

This theorem is referenced by: zfz1iso 10776

W3C validator