zfz1isolem1 - Intuitionistic Logic Explorer

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

Theorem zfz1isolem1 11270

Description: Lemma for zfz1iso 11271. 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 3367	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ⊆ ℤ)
3		zfz1isolem1.xf	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ Fin)
4		zfz1isolem1.mx	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ 𝑋)
5		diffisn 7187	. . . . . 6 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin)
6	3, 4, 5	syl2anc 415	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin)
7		zfz1isolem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ω)
8		zfz1isolem1.xs	. . . . . 6 ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)
9		dif1en 7173	. . . . . 6 ⊢ ((𝐾 ∈ ω ∧ 𝑋 ≈ suc 𝐾 ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ≈ 𝐾)
10	7, 8, 4, 9	syl3anc 1278	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ≈ 𝐾)
11	2, 6, 10	jca31 309	. . . 4 ⊢ (𝜑 → (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾))
12		zfz1isolem1.h	. . . . 5 ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))
13		sseq1 3271	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ⊆ ℤ ↔ (𝑋 ∖ {𝑀}) ⊆ ℤ))
14		eleq1 2301	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ∈ Fin ↔ (𝑋 ∖ {𝑀}) ∈ Fin))
15	13, 14	anbi12d 477	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ↔ ((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin)))
16		breq1 4128	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾))
17	15, 16	anbi12d 477	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)))
18		fveq2 5690	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀})))
19	18	oveq2d 6091	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))))
20		isoeq4 6000	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
21	19, 20	syl 14	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
22		isoeq5 6001	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
23	21, 22	bitrd 188	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
24	23	exbidv 1878	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
25	17, 24	imbi12d 234	. . . . . . 7 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) ↔ ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))))
26	25	spcgv 2912	. . . . . 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 5997	. . . 4 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))
31	30	cbvexv 1974	. . 3 ⊢ (∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
32	29, 31	sylib 122	. 2 ⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
33		df-isom 5381	. . . . . . . . 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 11198	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ₀)
38	3, 37	syl 14	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ₀)
39	38	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (♯‘𝑋) ∈ ℕ₀)
40	4	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑀 ∈ 𝑋)
41		f1osng 5677	. . . . . . 7 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
42	39, 40, 41	syl2anc 415	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
43		hashdifsn 11238	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
44	3, 4, 43	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
45	44	oveq1d 6090	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) + 1))
46	38	nn0cnd 9601	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
47		1cnd 8332	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
48	46, 47	npcand 8631	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
49	45, 48	eqtrd 2271	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋))
50	49	sneqd 3718	. . . . . . . . 9 ⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)})
51	50	ineq2d 3432	. . . . . . . 8 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}))
52		fzp1disj 10465	. . . . . . . 8 ⊢ ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅
53	51, 52	eqtr3di 2286	. . . . . . 7 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
54	53	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
55		incom 3421	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀}))
56		disjdif 3596	. . . . . . . 8 ⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅
57	55, 56	eqtri 2259	. . . . . . 7 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅
58	57	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)
59		f1oun 5654	. . . . . 6 ⊢ (((𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀}) ∧ (((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅ ∧ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
60	36, 42, 54, 58, 59	syl22anc 1279	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))
61	3, 4	zfz1isolemsplit 11268	. . . . . . 7 ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))
62		fidifsnid 7163	. . . . . . . . 9 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
63	3, 4, 62	syl2anc 415	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
64	63	eqcomd 2244	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀}))
65		f1oeq23 5625	. . . . . . 7 ⊢ (((1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}) ∧ 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀})) → ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})))
66	61, 64, 65	syl2anc 415	. . . . . 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 492	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ∈ Fin)
70	1	ad2antrr 492	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ⊆ ℤ)
71	4	ad2antrr 492	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑀 ∈ 𝑋)
72		zfz1isolem1.m	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
73	72	ad2antrr 492	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)
74		simplr 533	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))
75		simprl 535	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑎 ∈ (1...(♯‘𝑋)))
76		simprr 537	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑏 ∈ (1...(♯‘𝑋)))
77	69, 70, 71, 73, 74, 75, 76	zfz1isolemiso 11269	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
78	77	ralrimivva 2632	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
79		df-isom 5381	. . . 4 ⊢ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}):(1...(♯‘𝑋))–1-1-onto→𝑋 ∧ ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏))))
80	68, 78, 79	sylanbrc 421	. . 3 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋))
81		vex 2824	. . . . . . 7 ⊢ 𝑔 ∈ V
82	81	a1i 9	. . . . . 6 ⊢ (𝜑 → 𝑔 ∈ V)
83		opexg 4363	. . . . . . . 8 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
84	38, 4, 83	syl2anc 415	. . . . . . 7 ⊢ (𝜑 → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
85		snexg 4316	. . . . . . 7 ⊢ (⟨(♯‘𝑋), 𝑀⟩ ∈ V → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
86	84, 85	syl 14	. . . . . 6 ⊢ (𝜑 → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
87		unexg 4584	. . . . . 6 ⊢ ((𝑔 ∈ V ∧ {⟨(♯‘𝑋), 𝑀⟩} ∈ V) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
88	82, 86, 87	syl2anc 415	. . . . 5 ⊢ (𝜑 → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
89		isoeq1 5997	. . . . . 6 ⊢ (𝑓 = (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) → (𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) Isom < , < ((1...(♯‘𝑋)), 𝑋)))
90	89	spcegv 2913	. . . . 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 1954	1 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1400 = wceq 1402 ∃wex 1545 ∈ wcel 2209 ∀wral 2528 Vcvv 2821 ∖ cdif 3217 ∪ cun 3218 ∩ cin 3219 ⊆ wss 3220 ∅c0 3520 {csn 3705 ⟨cop 3708 class class class wbr 4125 suc csuc 4505 ωcom 4732 –1-1-onto→wf1o 5371 ‘cfv 5372 Isom wiso 5373 (class class class)co 6075 ≈ cen 7010 Fincfn 7012 1c1 8170 + caddc 8172 < clt 8350 ≤ cle 8351 − cmin 8487 ℕ₀cn0 9542 ℤcz 9623 ...cfz 10390 ♯chash 11192

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 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 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730 ax-cnex 8260 ax-resscn 8261 ax-1cn 8262 ax-1re 8263 ax-icn 8264 ax-addcl 8265 ax-addrcl 8266 ax-mulcl 8267 ax-addcom 8269 ax-addass 8271 ax-distr 8273 ax-i2m1 8274 ax-0lt1 8275 ax-0id 8277 ax-rnegex 8278 ax-cnre 8280 ax-pre-ltirr 8281 ax-pre-ltwlin 8282 ax-pre-lttrn 8283 ax-pre-apti 8284 ax-pre-ltadd 8285

This theorem 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-nel 2516 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-if 3636 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-id 4433 df-iord 4506 df-on 4508 df-ilim 4509 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-isom 5381 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-1st 6364 df-2nd 6365 df-recs 6566 df-irdg 6631 df-frec 6652 df-1o 6677 df-oadd 6681 df-er 6797 df-en 7013 df-dom 7014 df-fin 7015 df-pnf 8352 df-mnf 8353 df-xr 8354 df-ltxr 8355 df-le 8356 df-sub 8489 df-neg 8490 df-inn 9284 df-n0 9543 df-z 9624 df-uz 9901 df-fz 10391 df-ihash 11193

This theorem is referenced by: zfz1iso 11271

W3C validator