fzisoeu - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fzisoeu		Structured version Visualization version GIF version

Theorem fzisoeu 46316

Description: A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 14607 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fzisoeu.h	⊢ (𝜑 → 𝐻 ∈ Fin)
fzisoeu.or	⊢ (𝜑 → < Or 𝐻)
fzisoeu.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
fzisoeu.4	⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1))

**Assertion**
Ref	Expression
fzisoeu	⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))

Distinct variable groups: 𝑓,𝐻 𝑓,𝑀 𝑓,𝑁 Allowed substitution hint: 𝜑(𝑓)

Proof of Theorem fzisoeu Dummy variables 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzssz 13658	. . . . . . . . 9 ⊢ (𝑀...𝑁) ⊆ ℤ
2		zssre 12700	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3917	. . . . . . . 8 ⊢ (𝑀...𝑁) ⊆ ℝ
4		ltso 11390	. . . . . . . 8 ⊢ < Or ℝ
5		soss 5578	. . . . . . . 8 ⊢ ((𝑀...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (𝑀...𝑁)))
6	3, 4, 5	mp2 9	. . . . . . 7 ⊢ < Or (𝑀...𝑁)
7		fzfi 14115	. . . . . . 7 ⊢ (𝑀...𝑁) ∈ Fin
8		fz1iso 14607	. . . . . . 7 ⊢ (( < Or (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → ∃ℎ ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)))
9	6, 7, 8	mp2an 705	. . . . . 6 ⊢ ∃ℎ ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁))
10		fzisoeu.4	. . . . . . . . . . . . . . . 16 ⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1))
11		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻 = ∅ → (♯‘𝐻) = (♯‘∅))
12		hash0 14511	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
13	11, 12	eqtrdi 2811	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 = ∅ → (♯‘𝐻) = 0)
14	13	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 = ∅ → ((♯‘𝐻) + (𝑀 − 1)) = (0 + (𝑀 − 1)))
15	10, 14	eqtrid 2807	. . . . . . . . . . . . . . 15 ⊢ (𝐻 = ∅ → 𝑁 = (0 + (𝑀 − 1)))
16	15	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝐻 = ∅ → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1))))
17	16	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1))))
18		fzisoeu.m	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	zcnd 12804	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ ℂ)
20		1cnd 11302	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
21	19, 20	subcld 11669	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
22	21	addlidd 11511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 + (𝑀 − 1)) = (𝑀 − 1))
23	22	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀...(0 + (𝑀 − 1))) = (𝑀...(𝑀 − 1)))
24	18	zred 12803	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
25	24	ltm1d 12249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
26		peano2zm 12739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	18, 26	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28		fzn 13673	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
29	18, 27, 28	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
30	25, 29	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅)
31	23, 30	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀...(0 + (𝑀 − 1))) = ∅)
32	31	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...(0 + (𝑀 − 1))) = ∅)
33		eqcom 2767	. . . . . . . . . . . . . 14 ⊢ (𝐻 = ∅ ↔ ∅ = 𝐻)
34	33	bilani 510	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 = ∅) → ∅ = 𝐻)
35	17, 32, 34	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...𝑁) = 𝐻)
36	35	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (♯‘(𝑀...𝑁)) = (♯‘𝐻))
37	20, 19	pncan3d 11672	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
38	37	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 = (1 + (𝑀 − 1)))
39	38	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 = (1 + (𝑀 − 1)))
40		1red 11309	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ∈ ℝ)
41		neqne 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐻 = ∅ → 𝐻 ≠ ∅)
42	41	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ≠ ∅)
43		fzisoeu.h	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐻 ∈ Fin)
44	43	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ∈ Fin)
45		hashnncl 14510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
46	44, 45	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
47	42, 46	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘𝐻) ∈ ℕ)
48	47	nnred 12350	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘𝐻) ∈ ℝ)
49	27	zred 12803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
50	49	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑀 − 1) ∈ ℝ)
51	47	nnge1d 12386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ≤ (♯‘𝐻))
52	40, 48, 50, 51	leadd1dd 11930	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ ((♯‘𝐻) + (𝑀 − 1)))
53	52, 10	breqtrrdi 5146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ 𝑁)
54	39, 53	eqbrtrd 5126	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ≤ 𝑁)
55	18	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ∈ ℤ)
56		hashcl 14500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
57		nn0z 12717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐻) ∈ ℕ₀ → (♯‘𝐻) ∈ ℤ)
58	43, 56, 57	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
59	58, 27	zaddcld 12807	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) + (𝑀 − 1)) ∈ ℤ)
60	10, 59	eqeltrid 2864	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
61	60	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ ℤ)
62		eluz 12979	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
63	55, 61, 62	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑁 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
64	54, 63	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ (ℤ_≥‘𝑀))
65		hashfz 14572	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (♯‘(𝑀...𝑁)) = ((𝑁 − 𝑀) + 1))
66	64, 65	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘(𝑀...𝑁)) = ((𝑁 − 𝑀) + 1))
67	10	oveq1i 7430	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 − 𝑀) = (((♯‘𝐻) + (𝑀 − 1)) − 𝑀)
68	43, 56	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
69	68	nn0cnd 12669	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘𝐻) ∈ ℂ)
70	69, 21, 19	addsubassd 11689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((♯‘𝐻) + (𝑀 − 1)) − 𝑀) = ((♯‘𝐻) + ((𝑀 − 1) − 𝑀)))
71	67, 70	eqtrid 2807	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 𝑀) = ((♯‘𝐻) + ((𝑀 − 1) − 𝑀)))
72	20	negcld 11656	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -1 ∈ ℂ)
73	19, 20	negsubd 11675	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + -1) = (𝑀 − 1))
74	19, 72, 73	mvlladdcd 11726	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 − 1) − 𝑀) = -1)
75	74	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝐻) + ((𝑀 − 1) − 𝑀)) = ((♯‘𝐻) + -1))
76	71, 75	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 𝑀) = ((♯‘𝐻) + -1))
77	76	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (((♯‘𝐻) + -1) + 1))
78	77	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → ((𝑁 − 𝑀) + 1) = (((♯‘𝐻) + -1) + 1))
79	69, 20	negsubd 11675	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐻) + -1) = ((♯‘𝐻) − 1))
80	69, 20, 79	mvrrsubd 11729	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐻) + -1) + 1) = (♯‘𝐻))
81	80	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (((♯‘𝐻) + -1) + 1) = (♯‘𝐻))
82	66, 78, 81	3eqtrd 2799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘(𝑀...𝑁)) = (♯‘𝐻))
83	36, 82	pm2.61dan 825	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(𝑀...𝑁)) = (♯‘𝐻))
84	83	oveq2d 7436	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘(𝑀...𝑁))) = (1...(♯‘𝐻)))
85		isoeq4 7328	. . . . . . . . 9 ⊢ ((1...(♯‘(𝑀...𝑁))) = (1...(♯‘𝐻)) → (ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
86	84, 85	syl 18	. . . . . . . 8 ⊢ (𝜑 → (ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
87	86	biimpd 232	. . . . . . 7 ⊢ (𝜑 → (ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) → ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
88	87	eximdv 1949	. . . . . 6 ⊢ (𝜑 → (∃ℎ ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) → ∃ℎ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
89	9, 88	mpi 21	. . . . 5 ⊢ (𝜑 → ∃ℎ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)))
90		fzisoeu.or	. . . . . 6 ⊢ (𝜑 → < Or 𝐻)
91		fz1iso 14607	. . . . . 6 ⊢ (( < Or 𝐻 ∧ 𝐻 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))
92	90, 43, 91	syl2anc 596	. . . . 5 ⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))
93		exdistrv 1987	. . . . 5 ⊢ (∃ℎ∃𝑔(ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) ↔ (∃ℎ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)))
94	89, 92, 93	sylanbrc 595	. . . 4 ⊢ (𝜑 → ∃ℎ∃𝑔(ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)))
95		isocnv 7338	. . . . . . . 8 ⊢ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) → ^◡ℎ Isom < , < ((𝑀...𝑁), (1...(♯‘𝐻))))
96	95	ad2antrl 741	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))) → ^◡ℎ Isom < , < ((𝑀...𝑁), (1...(♯‘𝐻))))
97		simprr 785	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))) → 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))
98		isotr 7344	. . . . . . 7 ⊢ ((^◡ℎ Isom < , < ((𝑀...𝑁), (1...(♯‘𝐻))) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) → (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))
99	96, 97, 98	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))) → (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))
100	99	ex 418	. . . . 5 ⊢ (𝜑 → ((ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) → (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)))
101	100	2eximdv 1951	. . . 4 ⊢ (𝜑 → (∃ℎ∃𝑔(ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) → ∃ℎ∃𝑔(𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)))
102	94, 101	mpd 16	. . 3 ⊢ (𝜑 → ∃ℎ∃𝑔(𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))
103		vex 3454	. . . . . . 7 ⊢ 𝑔 ∈ V
104		vex 3454	. . . . . . . 8 ⊢ ℎ ∈ V
105	104	cnvex 7937	. . . . . . 7 ⊢ ^◡ℎ ∈ V
106	103, 105	coex 7942	. . . . . 6 ⊢ (𝑔 ∘ ^◡ℎ) ∈ V
107		isoeq1 7325	. . . . . 6 ⊢ (𝑓 = (𝑔 ∘ ^◡ℎ) → (𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)))
108	106, 107	spcev 3560	. . . . 5 ⊢ ((𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
109	108	a1i 11	. . . 4 ⊢ (𝜑 → ((𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
110	109	exlimdvv 1966	. . 3 ⊢ (𝜑 → (∃ℎ∃𝑔(𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
111	102, 110	mpd 16	. 2 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
112		ltwefz 14106	. . 3 ⊢ < We (𝑀...𝑁)
113		wemoiso 7985	. . 3 ⊢ ( < We (𝑀...𝑁) → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
114	112, 113	mp1i 14	. 2 ⊢ (𝜑 → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
115		df-eu 2594	. 2 ⊢ (∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ∧ ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
116	111, 114, 115	sylanbrc 595	1 ⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ∃*wmo 2562 ∃!weu 2593 ≠ wne 2955 ⊆ wss 3895 ∅c0 4278 class class class wbr 5102 Or wor 5557 We wwe 5602 ^◡ccnv 5649 ∘ ccom 5654 ‘cfv 6538 Isom wiso 6539 (class class class)co 7420 Fincfn 8973 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 < clt 11343 ≤ cle 11344 − cmin 11541 -cneg 11542 ℕcn 12335 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ...cfz 13639 ♯chash 14474

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-n0 12607 df-z 12694 df-uz 12966 df-fz 13640 df-hash 14475

This theorem is used by: fourierdlem36 47153

W3C validator