zfz1isolem1 - Intuitionistic Logic Explorer

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

Theorem zfz1isolem1 11216

Description: Lemma for zfz1iso 11217. 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 3359	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ⊆ ℤ)
3		zfz1isolem1.xf	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
4		zfz1isolem1.mx	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ 𝑋)
5		diffisn 7152	. . . . . 6 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin)
6	3, 4, 5	syl2anc 411	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin)
7		zfz1isolem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ω)
8		zfz1isolem1.xs	. . . . . 6 ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)
9		dif1en 7138	. . . . . 6 ⊢ ((𝐾 ∈ ω ∧ 𝑋 ≈ suc 𝐾 ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ≈ 𝐾)
10	7, 8, 4, 9	syl3anc 1274	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ≈ 𝐾)
11	2, 6, 10	jca31 309	. . . 4 ⊢ (𝜑 → (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾))
12		zfz1isolem1.h	. . . . 5 ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))
13		sseq1 3263	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ⊆ ℤ ↔ (𝑋 ∖ {𝑀}) ⊆ ℤ))
14		eleq1 2297	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ∈ Fin ↔ (𝑋 ∖ {𝑀}) ∈ Fin))
15	13, 14	anbi12d 473	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ↔ ((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin)))
16		breq1 4114	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾))
17	15, 16	anbi12d 473	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)))
18		fveq2 5672	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀})))
19	18	oveq2d 6068	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))))
20		isoeq4 5979	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
21	19, 20	syl 14	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
22		isoeq5 5980	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
23	21, 22	bitrd 188	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
24	23	exbidv 1874	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
25	17, 24	imbi12d 234	. . . . . . 7 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) ↔ ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))))
26	25	spcgv 2906	. . . . . 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 5976	. . . 4 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
31	30	cbvexv 1970	. . 3 ⊢ (∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
32	29, 31	sylib 122	. 2 ⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
33		df-isom 5363	. . . . . . . . 9 ⊢ (𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣))))
34	33	biimpi 120	. . . . . . . 8 ⊢ (𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) → (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣))))
35	34	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣))))
36	35	simpld 112	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}))
37		hashcl 11148	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ₀)
38	3, 37	syl 14	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ₀)
39	38	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (♯‘𝑋) ∈ ℕ₀)
40	4	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑀 ∈ 𝑋)
41		f1osng 5659	. . . . . . 7 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
42	39, 40, 41	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
43		hashdifsn 11188	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
44	3, 4, 43	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
45	44	oveq1d 6067	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) + 1))
46	38	nn0cnd 9557	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
47		1cnd 8292	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
48	46, 47	npcand 8590	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
49	45, 48	eqtrd 2267	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋))
50	49	sneqd 3704	. . . . . . . . 9 ⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)})
51	50	ineq2d 3424	. . . . . . . 8 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}))
52		fzp1disj 10418	. . . . . . . 8 ⊢ ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅
53	51, 52	eqtr3di 2282	. . . . . . 7 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
54	53	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
55		incom 3413	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀}))
56		disjdif 3583	. . . . . . . 8 ⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅
57	55, 56	eqtri 2255	. . . . . . 7 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅
58	57	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)
59		f1oun 5636	. . . . . 6 ⊢ (((𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀}) ∧ (((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅ ∧ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
60	36, 42, 54, 58, 59	syl22anc 1275	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
61	3, 4	zfz1isolemsplit 11214	. . . . . . 7 ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))
62		fidifsnid 7128	. . . . . . . . 9 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
63	3, 4, 62	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
64	63	eqcomd 2240	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀}))
65		f1oeq23 5607	. . . . . . 7 ⊢ (((1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}) ∧ 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀})) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
66	61, 64, 65	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
67	66	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
68	60, 67	mpbird 167	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋)
69	3	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ∈ Fin)
70	1	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ⊆ ℤ)
71	4	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑀 ∈ 𝑋)
72		zfz1isolem1.m	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
73	72	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
74		simplr 529	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
75		simprl 531	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑎 ∈ (1...(♯‘𝑋)))
76		simprr 533	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑏 ∈ (1...(♯‘𝑋)))
77	69, 70, 71, 73, 74, 75, 76	zfz1isolemiso 11215	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
78	77	ralrimivva 2626	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
79		df-isom 5363	. . . 4 ⊢ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ∧ ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏))))
80	68, 78, 79	sylanbrc 417	. . 3 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋))
81		vex 2818	. . . . . . 7 ⊢ 𝑔 ∈ V
82	81	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝑔 ∈ V)
83		opexg 4346	. . . . . . . 8 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
84	38, 4, 83	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
85		snexg 4299	. . . . . . 7 ⊢ (⟨(♯‘𝑋), 𝑀⟩ ∈ V → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
86	84, 85	syl 14	. . . . . 6 ⊢ (𝜑 → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
87		unexg 4566	. . . . . 6 ⊢ ((𝑔 ∈ V ∧ {⟨(♯‘𝑋), 𝑀⟩} ∈ V) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
88	82, 86, 87	syl2anc 411	. . . . 5 ⊢ (𝜑 → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
89		isoeq1 5976	. . . . . 6 ⊢ (𝑓 = (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) → (𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋)))
90	89	spcegv 2907	. . . . 5 ⊢ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)))
91	88, 90	syl 14	. . . 4 ⊢ (𝜑 → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)))
92	91	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)))
93	80, 92	mpd 13	. 2 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))
94	32, 93	exlimddv 1950	1 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1396 = wceq 1398 ∃wex 1541 ∈ wcel 2205 ∀wral 2522 Vcvv 2815 ∖ cdif 3210 ∪ cun 3211 ∩ cin 3212 ⊆ wss 3213 ∅c0 3510 {csn 3691 ⟨cop 3694 class class class wbr 4111 suc csuc 4488 ωcom 4714 –1-1-onto→wf1o 5353 ‘cfv 5354 Isom wiso 5355 (class class class)co 6052 ≈ cen 6975 Fincfn 6977 1c1 8130 + caddc 8132 < clt 8310 ≤ cle 8311 − cmin 8446 ℕ₀cn0 9498 ℤcz 9579 ...cfz 10345 ♯chash 11142

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4227 ax-sep 4230 ax-nul 4238 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-iinf 4712 ax-cnex 8220 ax-resscn 8221 ax-1cn 8222 ax-1re 8223 ax-icn 8224 ax-addcl 8225 ax-addrcl 8226 ax-mulcl 8227 ax-addcom 8229 ax-addass 8231 ax-distr 8233 ax-i2m1 8234 ax-0lt1 8235 ax-0id 8237 ax-rnegex 8238 ax-cnre 8240 ax-pre-ltirr 8241 ax-pre-ltwlin 8242 ax-pre-lttrn 8243 ax-pre-apti 8244 ax-pre-ltadd 8245

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rab 2531 df-v 2817 df-sbc 3045 df-csb 3141 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-nul 3511 df-if 3623 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-int 3952 df-iun 3995 df-br 4112 df-opab 4174 df-mpt 4175 df-tr 4211 df-id 4416 df-iord 4489 df-on 4491 df-ilim 4492 df-suc 4494 df-iom 4715 df-xp 4757 df-rel 4758 df-cnv 4759 df-co 4760 df-dm 4761 df-rn 4762 df-res 4763 df-ima 4764 df-iota 5314 df-fun 5356 df-fn 5357 df-f 5358 df-f1 5359 df-fo 5360 df-f1o 5361 df-fv 5362 df-isom 5363 df-riota 6005 df-ov 6055 df-oprab 6056 df-mpo 6057 df-1st 6336 df-2nd 6337 df-recs 6538 df-irdg 6603 df-frec 6624 df-1o 6649 df-oadd 6653 df-er 6769 df-en 6978 df-dom 6979 df-fin 6980 df-pnf 8312 df-mnf 8313 df-xr 8314 df-ltxr 8315 df-le 8316 df-sub 8448 df-neg 8449 df-inn 9240 df-n0 9499 df-z 9580 df-uz 9857 df-fz 10346 df-ihash 11143

This theorem is referenced by: zfz1iso 11217

W3C validator