Theorem smoiso 6302

Description: If 𝐹 is an isomorphism from an ordinal 𝐴 onto 𝐵, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)

Assertion

Ref	Expression
smoiso	⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹)

Proof of Theorem smoiso

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isof1o 5807	. . . 4 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
2		f1of 5461	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 14	. . 3 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵)
4		ffdm 5386	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
5	4	simpld 112	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:dom 𝐹⟶𝐵)
6		fss 5377	. . . . 5 ⊢ ((𝐹:dom 𝐹⟶𝐵 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
7	5, 6	sylan 283	. . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
8	7	3adant2 1016	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
9	3, 8	syl3an1 1271	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
10		fdm 5371	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
11	10	eqcomd 2183	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = dom 𝐹)
12		ordeq 4372	. . . . 5 ⊢ (𝐴 = dom 𝐹 → (Ord 𝐴 ↔ Ord dom 𝐹))
13	1, 2, 11, 12	4syl 18	. . . 4 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → (Ord 𝐴 ↔ Ord dom 𝐹))
14	13	biimpa 296	. . 3 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴) → Ord dom 𝐹)
15	14	3adant3 1017	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Ord dom 𝐹)
16	10	eleq2d 2247	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
17	10	eleq2d 2247	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴))
18	16, 17	anbi12d 473	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)))
19	1, 2, 18	3syl 17	. . . . 5 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)))
20		epel 4292	. . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)
21		isorel 5808	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 E 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦)))
22	20, 21	bitr3id 194	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑥) E (𝐹‘𝑦)))
23		ffn 5365	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
24	3, 23	syl 14	. . . . . . . . . 10 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
25	24	adantr 276	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝐹 Fn 𝐴)
26		simprr 531	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
27		funfvex 5532	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ V)
28	27	funfni 5316	. . . . . . . . . 10 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
29		epelg 4290	. . . . . . . . . 10 ⊢ ((𝐹‘𝑦) ∈ V → ((𝐹‘𝑥) E (𝐹‘𝑦) ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
30	28, 29	syl 14	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) E (𝐹‘𝑦) ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
31	25, 26, 30	syl2anc 411	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥) E (𝐹‘𝑦) ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
32	22, 31	bitrd 188	. . . . . . 7 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 ↔ (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
33	32	biimpd 144	. . . . . 6 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
34	33	ex 115	. . . . 5 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦))))
35	19, 34	sylbid 150	. . . 4 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦))))
36	35	ralrimivv 2558	. . 3 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹(𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
37	36	3ad2ant1 1018	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹(𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦)))
38		df-smo 6286	. 2 ⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹(𝑥 ∈ 𝑦 → (𝐹‘𝑥) ∈ (𝐹‘𝑦))))
39	9, 15, 37, 38	syl3anbrc 1181	1 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  ∀wral 2455  Vcvv 2737   ⊆ wss 3129   class class class wbr 4003   E cep 4287  Ord word 4362  Oncon0 4363  dom cdm 4626   Fn wfn 5211  ⟶wf 5212  –1-1-onto→wf1o 5215  ‘cfv 5216   Isom wiso 5217  Smo wsmo 6285

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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-tr 4102  df-eprel 4289  df-id 4293  df-iord 4366  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-f1o 5223  df-fv 5224  df-isom 5225  df-smo 6286

This theorem is referenced by: (None)