zfz1isolem1 - Intuitionistic Logic Explorer

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

Theorem zfz1isolem1 10749

Description: Lemma for zfz1iso 10750. 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 3259	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ⊆ ℤ)
3		zfz1isolem1.xf	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
4		zfz1isolem1.mx	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ 𝑋)
5		diffisn 6855	. . . . . 6 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin)
6	3, 4, 5	syl2anc 409	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin)
7		zfz1isolem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ω)
8		zfz1isolem1.xs	. . . . . 6 ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)
9		dif1en 6841	. . . . . 6 ⊢ ((𝐾 ∈ ω ∧ 𝑋 ≈ suc 𝐾 ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ≈ 𝐾)
10	7, 8, 4, 9	syl3anc 1228	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ≈ 𝐾)
11	2, 6, 10	jca31 307	. . . 4 ⊢ (𝜑 → (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾))
12		zfz1isolem1.h	. . . . 5 ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))
13		sseq1 3164	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ⊆ ℤ ↔ (𝑋 ∖ {𝑀}) ⊆ ℤ))
14		eleq1 2228	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ∈ Fin ↔ (𝑋 ∖ {𝑀}) ∈ Fin))
15	13, 14	anbi12d 465	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ↔ ((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin)))
16		breq1 3984	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾))
17	15, 16	anbi12d 465	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)))
18		fveq2 5485	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀})))
19	18	oveq2d 5857	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))))
20		isoeq4 5771	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
21	19, 20	syl 14	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
22		isoeq5 5772	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
23	21, 22	bitrd 187	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
24	23	exbidv 1813	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
25	17, 24	imbi12d 233	. . . . . . 7 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) ↔ ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))))
26	25	spcgv 2812	. . . . . 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 5768	. . . 4 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
31	30	cbvexv 1906	. . 3 ⊢ (∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
32	29, 31	sylib 121	. 2 ⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
33		df-isom 5196	. . . . . . . . 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 10690	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ₀)
38	3, 37	syl 14	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ₀)
39	38	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (♯‘𝑋) ∈ ℕ₀)
40	4	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑀 ∈ 𝑋)
41		f1osng 5472	. . . . . . 7 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
42	39, 40, 41	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
43		hashdifsn 10728	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
44	3, 4, 43	syl2anc 409	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
45	44	oveq1d 5856	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) + 1))
46	38	nn0cnd 9165	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
47		1cnd 7911	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
48	46, 47	npcand 8209	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
49	45, 48	eqtrd 2198	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋))
50	49	sneqd 3588	. . . . . . . . 9 ⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)})
51	50	ineq2d 3322	. . . . . . . 8 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}))
52		fzp1disj 10011	. . . . . . . 8 ⊢ ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅
53	51, 52	eqtr3di 2213	. . . . . . 7 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
54	53	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
55		incom 3313	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀}))
56		disjdif 3480	. . . . . . . 8 ⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅
57	55, 56	eqtri 2186	. . . . . . 7 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅
58	57	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)
59		f1oun 5451	. . . . . 6 ⊢ (((𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀}) ∧ (((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅ ∧ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
60	36, 42, 54, 58, 59	syl22anc 1229	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
61	3, 4	zfz1isolemsplit 10747	. . . . . . 7 ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))
62		fidifsnid 6833	. . . . . . . . 9 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
63	3, 4, 62	syl2anc 409	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
64	63	eqcomd 2171	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀}))
65		f1oeq23 5423	. . . . . . 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 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ∈ Fin)
70	1	ad2antrr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ⊆ ℤ)
71	4	ad2antrr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑀 ∈ 𝑋)
72		zfz1isolem1.m	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
73	72	ad2antrr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
74		simplr 520	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
75		simprl 521	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑎 ∈ (1...(♯‘𝑋)))
76		simprr 522	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑏 ∈ (1...(♯‘𝑋)))
77	69, 70, 71, 73, 74, 75, 76	zfz1isolemiso 10748	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
78	77	ralrimivva 2547	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
79		df-isom 5196	. . . 4 ⊢ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ∧ ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏))))
80	68, 78, 79	sylanbrc 414	. . 3 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋))
81		vex 2728	. . . . . . 7 ⊢ 𝑔 ∈ V
82	81	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝑔 ∈ V)
83		opexg 4205	. . . . . . . 8 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
84	38, 4, 83	syl2anc 409	. . . . . . 7 ⊢ (𝜑 → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
85		snexg 4162	. . . . . . 7 ⊢ (⟨(♯‘𝑋), 𝑀⟩ ∈ V → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
86	84, 85	syl 14	. . . . . 6 ⊢ (𝜑 → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
87		unexg 4420	. . . . . 6 ⊢ ((𝑔 ∈ V ∧ {⟨(♯‘𝑋), 𝑀⟩} ∈ V) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
88	82, 86, 87	syl2anc 409	. . . . 5 ⊢ (𝜑 → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
89		isoeq1 5768	. . . . . 6 ⊢ (𝑓 = (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) → (𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋)))
90	89	spcegv 2813	. . . . 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 1886	1 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1341 = wceq 1343 ∃wex 1480 ∈ wcel 2136 ∀wral 2443 Vcvv 2725 ∖ cdif 3112 ∪ cun 3113 ∩ cin 3114 ⊆ wss 3115 ∅c0 3408 {csn 3575 ⟨cop 3578 class class class wbr 3981 suc csuc 4342 ωcom 4566 –1-1-onto→wf1o 5186 ‘cfv 5187 Isom wiso 5188 (class class class)co 5841 ≈ cen 6700 Fincfn 6702 1c1 7750 + caddc 7752 < clt 7929 ≤ cle 7930 − cmin 8065 ℕ₀cn0 9110 ℤcz 9187 ...cfz 9940 ♯chash 10684

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4096 ax-sep 4099 ax-nul 4107 ax-pow 4152 ax-pr 4186 ax-un 4410 ax-setind 4513 ax-iinf 4564 ax-cnex 7840 ax-resscn 7841 ax-1cn 7842 ax-1re 7843 ax-icn 7844 ax-addcl 7845 ax-addrcl 7846 ax-mulcl 7847 ax-addcom 7849 ax-addass 7851 ax-distr 7853 ax-i2m1 7854 ax-0lt1 7855 ax-0id 7857 ax-rnegex 7858 ax-cnre 7860 ax-pre-ltirr 7861 ax-pre-ltwlin 7862 ax-pre-lttrn 7863 ax-pre-apti 7864 ax-pre-ltadd 7865

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2296 df-ne 2336 df-nel 2431 df-ral 2448 df-rex 2449 df-reu 2450 df-rab 2452 df-v 2727 df-sbc 2951 df-csb 3045 df-dif 3117 df-un 3119 df-in 3121 df-ss 3128 df-nul 3409 df-if 3520 df-pw 3560 df-sn 3581 df-pr 3582 df-op 3584 df-uni 3789 df-int 3824 df-iun 3867 df-br 3982 df-opab 4043 df-mpt 4044 df-tr 4080 df-id 4270 df-iord 4343 df-on 4345 df-ilim 4346 df-suc 4348 df-iom 4567 df-xp 4609 df-rel 4610 df-cnv 4611 df-co 4612 df-dm 4613 df-rn 4614 df-res 4615 df-ima 4616 df-iota 5152 df-fun 5189 df-fn 5190 df-f 5191 df-f1 5192 df-fo 5193 df-f1o 5194 df-fv 5195 df-isom 5196 df-riota 5797 df-ov 5844 df-oprab 5845 df-mpo 5846 df-1st 6105 df-2nd 6106 df-recs 6269 df-irdg 6334 df-frec 6355 df-1o 6380 df-oadd 6384 df-er 6497 df-en 6703 df-dom 6704 df-fin 6705 df-pnf 7931 df-mnf 7932 df-xr 7933 df-ltxr 7934 df-le 7935 df-sub 8067 df-neg 8068 df-inn 8854 df-n0 9111 df-z 9188 df-uz 9463 df-fz 9941 df-ihash 10685

This theorem is referenced by: zfz1iso 10750

W3C validator