zfz1isolem1 - Intuitionistic Logic Explorer

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

Theorem zfz1isolem1 11314

Description: Lemma for zfz1iso 11315. 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 7201	. . . . . 6 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin)
6	3, 4, 5	syl2anc 415	. . . . 5 ⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin)
7		zfz1isolem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ω)
8		zfz1isolem1.xs	. . . . . 6 ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)
9		dif1en 7187	. . . . . 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 4134	. . . . . . . . 9 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾))
17	15, 16	anbi12d 477	. . . . . . . 8 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)))
18		fveq2 5698	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀})))
19	18	oveq2d 6104	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))))
20		isoeq4 6013	. . . . . . . . . . 11 ⊢ ((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
21	19, 20	syl 14	. . . . . . . . . 10 ⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦)))
22		isoeq5 6014	. . . . . . . . . 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 6010	. . . 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 5389	. . . . . . . . 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 11242	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ₀)
38	3, 37	syl 14	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ₀)
39	38	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (♯‘𝑋) ∈ ℕ₀)
40	4	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑀 ∈ 𝑋)
41		f1osng 5685	. . . . . . 7 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
42	39, 40, 41	syl2anc 415	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {⟨(♯‘𝑋), 𝑀⟩}:{(♯‘𝑋)}–1-1-onto→{𝑀})
43		hashdifsn 11282	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
44	3, 4, 43	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1))
45	44	oveq1d 6103	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) + 1))
46	38	nn0cnd 9633	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
47		1cnd 8348	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
48	46, 47	npcand 8648	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) = (♯‘𝑋))
49	45, 48	eqtrd 2271	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋))
50	49	sneqd 3722	. . . . . . . . 9 ⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)})
51	50	ineq2d 3432	. . . . . . . 8 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}))
52		fzp1disj 10504	. . . . . . . 8 ⊢ ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅
53	51, 52	eqtr3di 2286	. . . . . . 7 ⊢ (𝜑 → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
54	53	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅)
55		incom 3421	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀}))
56		disjdif 3599	. . . . . . . 8 ⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅
57	55, 56	eqtri 2259	. . . . . . 7 ⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅
58	57	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)
59		f1oun 5662	. . . . . 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 11312	. . . . . . 7 ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))
62		fidifsnid 7177	. . . . . . . . 9 ⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
63	3, 4, 62	syl2anc 415	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋)
64	63	eqcomd 2244	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀}))
65		f1oeq23 5633	. . . . . . 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 11313	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
78	77	ralrimivva 2632	. . . 4 ⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑎) < ((𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝑏)))
79		df-isom 5389	. . . 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 4370	. . . . . . . 8 ⊢ (((♯‘𝑋) ∈ ℕ₀ ∧ 𝑀 ∈ 𝑋) → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
84	38, 4, 83	syl2anc 415	. . . . . . 7 ⊢ (𝜑 → ⟨(♯‘𝑋), 𝑀⟩ ∈ V)
85		snexg 4323	. . . . . . 7 ⊢ (⟨(♯‘𝑋), 𝑀⟩ ∈ V → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
86	84, 85	syl 14	. . . . . 6 ⊢ (𝜑 → {⟨(♯‘𝑋), 𝑀⟩} ∈ V)
87		unexg 4591	. . . . . 6 ⊢ ((𝑔 ∈ V ∧ {⟨(♯‘𝑋), 𝑀⟩} ∈ V) → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
88	82, 86, 87	syl2anc 415	. . . . 5 ⊢ (𝜑 → (𝑔 ∪ {⟨(♯‘𝑋), 𝑀⟩}) ∈ V)
89		isoeq1 6010	. . . . . 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

This proof depends on syntax axioms: → 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 3709 ⟨cop 3712 class class class wbr 4131 suc csuc 4512 ωcom 4739 –1-1-onto→wf1o 5379 ‘cfv 5380 Isom wiso 5381 (class class class)co 6088 ≈ cen 7024 Fincfn 7026 1c1 8186 + caddc 8188 < clt 8366 ≤ cle 8367 − cmin 8504 ℕ₀cn0 9574 ℤcz 9655 ...cfz 10428 ♯chash 11236

This proof depends on 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 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-addcom 8285 ax-addass 8287 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-0id 8293 ax-rnegex 8294 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301

This proof 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 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-oadd 6695 df-er 6811 df-en 7027 df-dom 7028 df-fin 7029 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-inn 9314 df-n0 9575 df-z 9656 df-uz 9938 df-fz 10429 df-ihash 11237

This theorem is used by: zfz1iso 11315

W3C validator