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 46118

Description: A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 14527 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 13580	. . . . . . . . 9 ⊢ (𝑀...𝑁) ⊆ ℤ
2		zssre 12623	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
3	1, 2	sstri 3943	. . . . . . . 8 ⊢ (𝑀...𝑁) ⊆ ℝ
4		ltso 11315	. . . . . . . 8 ⊢ < Or ℝ
5		soss 5587	. . . . . . . 8 ⊢ ((𝑀...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (𝑀...𝑁)))
6	3, 4, 5	mp2 9	. . . . . . 7 ⊢ < Or (𝑀...𝑁)
7		fzfi 14036	. . . . . . 7 ⊢ (𝑀...𝑁) ∈ Fin
8		fz1iso 14527	. . . . . . 7 ⊢ (( < Or (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → ∃ℎ ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)))
9	6, 7, 8	mp2an 705	. . . . . 6 ⊢ ∃ℎ ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁))
10		fzisoeu.4	. . . . . . . . . . . . . . . 16 ⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1))
11		fveq2 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻 = ∅ → (♯‘𝐻) = (♯‘∅))
12		hash0 14431	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
13	11, 12	eqtrdi 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 = ∅ → (♯‘𝐻) = 0)
14	13	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 = ∅ → ((♯‘𝐻) + (𝑀 − 1)) = (0 + (𝑀 − 1)))
15	10, 14	eqtrid 2809	. . . . . . . . . . . . . . 15 ⊢ (𝐻 = ∅ → 𝑁 = (0 + (𝑀 − 1)))
16	15	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ (𝐻 = ∅ → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1))))
17	16	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1))))
18		fzisoeu.m	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	zcnd 12727	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ ℂ)
20		1cnd 11227	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
21	19, 20	subcld 11594	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
22	21	addlidd 11436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 + (𝑀 − 1)) = (𝑀 − 1))
23	22	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀...(0 + (𝑀 − 1))) = (𝑀...(𝑀 − 1)))
24	18	zred 12726	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
25	24	ltm1d 12172	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
26		peano2zm 12662	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	18, 26	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28		fzn 13594	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
29	18, 27, 28	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
30	25, 29	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅)
31	23, 30	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀...(0 + (𝑀 − 1))) = ∅)
32	31	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...(0 + (𝑀 − 1))) = ∅)
33		eqcom 2769	. . . . . . . . . . . . . 14 ⊢ (𝐻 = ∅ ↔ ∅ = 𝐻)
34	33	bilani 510	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 = ∅) → ∅ = 𝐻)
35	17, 32, 34	3eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (𝑀...𝑁) = 𝐻)
36	35	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐻 = ∅) → (♯‘(𝑀...𝑁)) = (♯‘𝐻))
37	20, 19	pncan3d 11597	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
38	37	eqcomd 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 = (1 + (𝑀 − 1)))
39	38	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 = (1 + (𝑀 − 1)))
40		1red 11234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ∈ ℝ)
41		neqne 2965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐻 = ∅ → 𝐻 ≠ ∅)
42	41	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ≠ ∅)
43		fzisoeu.h	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐻 ∈ Fin)
44	43	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ∈ Fin)
45		hashnncl 14430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻 ∈ Fin → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
46	44, 45	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
47	42, 46	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘𝐻) ∈ ℕ)
48	47	nnred 12273	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘𝐻) ∈ ℝ)
49	27	zred 12726	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
50	49	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑀 − 1) ∈ ℝ)
51	47	nnge1d 12309	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ≤ (♯‘𝐻))
52	40, 48, 50, 51	leadd1dd 11853	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ ((♯‘𝐻) + (𝑀 − 1)))
53	52, 10	breqtrrdi 5151	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ 𝑁)
54	39, 53	eqbrtrd 5131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ≤ 𝑁)
55	18	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ∈ ℤ)
56		hashcl 14420	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
57		nn0z 12640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐻) ∈ ℕ₀ → (♯‘𝐻) ∈ ℤ)
58	43, 56, 57	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
59	58, 27	zaddcld 12730	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((♯‘𝐻) + (𝑀 − 1)) ∈ ℤ)
60	10, 59	eqeltrid 2866	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
61	60	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ ℤ)
62		eluz 12902	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
63	55, 61, 62	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑁 ∈ (ℤ_≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
64	54, 63	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ (ℤ_≥‘𝑀))
65		hashfz 14492	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (♯‘(𝑀...𝑁)) = ((𝑁 − 𝑀) + 1))
66	64, 65	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘(𝑀...𝑁)) = ((𝑁 − 𝑀) + 1))
67	10	oveq1i 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 − 𝑀) = (((♯‘𝐻) + (𝑀 − 1)) − 𝑀)
68	43, 56	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
69	68	nn0cnd 12592	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘𝐻) ∈ ℂ)
70	69, 21, 19	addsubassd 11614	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((♯‘𝐻) + (𝑀 − 1)) − 𝑀) = ((♯‘𝐻) + ((𝑀 − 1) − 𝑀)))
71	67, 70	eqtrid 2809	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 𝑀) = ((♯‘𝐻) + ((𝑀 − 1) − 𝑀)))
72	20	negcld 11581	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -1 ∈ ℂ)
73	19, 20	negsubd 11600	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + -1) = (𝑀 − 1))
74	73	eqcomd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) = (𝑀 + -1))
75	19, 72, 74	mvrladdd 11652	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 − 1) − 𝑀) = -1)
76	75	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝐻) + ((𝑀 − 1) − 𝑀)) = ((♯‘𝐻) + -1))
77	71, 76	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 𝑀) = ((♯‘𝐻) + -1))
78	77	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (((♯‘𝐻) + -1) + 1))
79	78	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → ((𝑁 − 𝑀) + 1) = (((♯‘𝐻) + -1) + 1))
80	69, 20	negsubd 11600	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝐻) + -1) = ((♯‘𝐻) − 1))
81	80	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐻) + -1) + 1) = (((♯‘𝐻) − 1) + 1))
82	69, 20	npcand 11598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((♯‘𝐻) − 1) + 1) = (♯‘𝐻))
83	81, 82	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐻) + -1) + 1) = (♯‘𝐻))
84	83	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (((♯‘𝐻) + -1) + 1) = (♯‘𝐻))
85	66, 79, 84	3eqtrd 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐻 = ∅) → (♯‘(𝑀...𝑁)) = (♯‘𝐻))
86	36, 85	pm2.61dan 825	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(𝑀...𝑁)) = (♯‘𝐻))
87	86	oveq2d 7432	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘(𝑀...𝑁))) = (1...(♯‘𝐻)))
88		isoeq4 7324	. . . . . . . . 9 ⊢ ((1...(♯‘(𝑀...𝑁))) = (1...(♯‘𝐻)) → (ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
89	87, 88	syl 18	. . . . . . . 8 ⊢ (𝜑 → (ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
90	89	biimpd 232	. . . . . . 7 ⊢ (𝜑 → (ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) → ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
91	90	eximdv 1950	. . . . . 6 ⊢ (𝜑 → (∃ℎ ℎ Isom < , < ((1...(♯‘(𝑀...𝑁))), (𝑀...𝑁)) → ∃ℎ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁))))
92	9, 91	mpi 21	. . . . 5 ⊢ (𝜑 → ∃ℎ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)))
93		fzisoeu.or	. . . . . 6 ⊢ (𝜑 → < Or 𝐻)
94		fz1iso 14527	. . . . . 6 ⊢ (( < Or 𝐻 ∧ 𝐻 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))
95	93, 43, 94	syl2anc 596	. . . . 5 ⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))
96		exdistrv 1988	. . . . 5 ⊢ (∃ℎ∃𝑔(ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) ↔ (∃ℎ ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)))
97	92, 95, 96	sylanbrc 595	. . . 4 ⊢ (𝜑 → ∃ℎ∃𝑔(ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)))
98		isocnv 7334	. . . . . . . 8 ⊢ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) → ^◡ℎ Isom < , < ((𝑀...𝑁), (1...(♯‘𝐻))))
99	98	ad2antrl 741	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))) → ^◡ℎ Isom < , < ((𝑀...𝑁), (1...(♯‘𝐻))))
100		simprr 785	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))) → 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))
101		isotr 7340	. . . . . . 7 ⊢ ((^◡ℎ Isom < , < ((𝑀...𝑁), (1...(♯‘𝐻))) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) → (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))
102	99, 100, 101	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻))) → (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))
103	102	ex 418	. . . . 5 ⊢ (𝜑 → ((ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) → (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)))
104	103	2eximdv 1952	. . . 4 ⊢ (𝜑 → (∃ℎ∃𝑔(ℎ Isom < , < ((1...(♯‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(♯‘𝐻)), 𝐻)) → ∃ℎ∃𝑔(𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)))
105	97, 104	mpd 16	. . 3 ⊢ (𝜑 → ∃ℎ∃𝑔(𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻))
106		vex 3457	. . . . . . 7 ⊢ 𝑔 ∈ V
107		vex 3457	. . . . . . . 8 ⊢ ℎ ∈ V
108	107	cnvex 7925	. . . . . . 7 ⊢ ^◡ℎ ∈ V
109	106, 108	coex 7930	. . . . . 6 ⊢ (𝑔 ∘ ^◡ℎ) ∈ V
110		isoeq1 7321	. . . . . 6 ⊢ (𝑓 = (𝑔 ∘ ^◡ℎ) → (𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻)))
111	109, 110	spcev 3563	. . . . 5 ⊢ ((𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
112	111	a1i 11	. . . 4 ⊢ (𝜑 → ((𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
113	112	exlimdvv 1967	. . 3 ⊢ (𝜑 → (∃ℎ∃𝑔(𝑔 ∘ ^◡ℎ) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
114	105, 113	mpd 16	. 2 ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
115		ltwefz 14027	. . 3 ⊢ < We (𝑀...𝑁)
116		wemoiso 7973	. . 3 ⊢ ( < We (𝑀...𝑁) → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
117	115, 116	mp1i 14	. 2 ⊢ (𝜑 → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
118		df-eu 2596	. 2 ⊢ (∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ∧ ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
119	114, 117, 118	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 1570 ∃wex 1812 ∈ wcel 2145 ∃*wmo 2564 ∃!weu 2595 ≠ wne 2957 ⊆ wss 3902 ∅c0 4282 class class class wbr 5107 Or wor 5566 We wwe 5611 ^◡ccnv 5658 ∘ ccom 5663 ‘cfv 6537 Isom wiso 6538 (class class class)co 7416 Fincfn 8955 ℝcr 11124 0cc0 11125 1c1 11126 + caddc 11128 < clt 11268 ≤ cle 11269 − cmin 11466 -cneg 11467 ℕcn 12258 ℕ₀cn0 12529 ℤcz 12616 ℤ_≥cuz 12888 ...cfz 13561 ♯chash 14394

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-oi 9485 df-card 9947 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-nn 12259 df-n0 12530 df-z 12617 df-uz 12889 df-fz 13562 df-hash 14395

This theorem is used by: fourierdlem36 46956

W3C validator