Metamath Proof Explorer

Theorem smogt

Description: A strictly monotone ordinal function is greater than or equal to its argument. Exercise 1 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 23-Nov-2011) (Revised by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion smogt ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ⊆ ( 𝐹 ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑥 = 𝐶 → 𝑥 = 𝐶 )
2 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
3 1 2 sseq12d ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ↔ 𝐶 ⊆ ( 𝐹 ‘ 𝐶 ) ) )
4 3 imbi2d ⊢ ( 𝑥 = 𝐶 → ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → 𝐶 ⊆ ( 𝐹 ‘ 𝐶 ) ) ) )
5 smodm2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 )
6 5 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝐴 )
7 simp3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
8 ordelord ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝑥 )
9 6 7 8 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → Ord 𝑥 )
10 vex ⊢ 𝑥 ∈ V
11 10 elon ⊢ ( 𝑥 ∈ On ↔ Ord 𝑥 )
12 9 11 sylibr ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
13 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
14 13 3anbi3d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) ) )
15 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
16 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
17 15 16 sseq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) )
18 14 17 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) )
19 simpl1 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 Fn 𝐴 )
20 simpl2 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → Smo 𝐹 )
21 ordtr1 ⊢ ( Ord 𝐴 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
22 21 expcomd ⊢ ( Ord 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) ) )
23 6 7 22 sylc ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) )
24 23 imp ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 )
25 pm2.27 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) )
26 19 20 24 25 syl3anc ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) )
27 26 ralimdva ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) )
28 5 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → Ord 𝐴 )
29 simp31 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 ∈ 𝐴 )
30 28 29 8 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → Ord 𝑥 )
31 simp32 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝑥 )
32 ordelord ⊢ ( ( Ord 𝑥 ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
33 30 31 32 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → Ord 𝑦 )
34 smofvon2 ⊢ ( Smo 𝐹 → ( 𝐹 ‘ 𝑥 ) ∈ On )
35 34 3ad2ant2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ On )
36 eloni ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ On → Ord ( 𝐹 ‘ 𝑥 ) )
37 35 36 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → Ord ( 𝐹 ‘ 𝑥 ) )
38 simp33 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) )
39 smoel2 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
40 39 3adantr3 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
41 40 3impa ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
42 ordtr2 ⊢ ( ( Ord 𝑦 ∧ Ord ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
43 42 imp ⊢ ( ( ( Ord 𝑦 ∧ Ord ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
44 33 37 38 41 43 syl22anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
45 44 3expia ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
46 45 3expd ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) ) )
47 46 3impia ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
48 47 imp ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) → 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
49 48 ralimdva ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
50 dfss3 ⊢ ( 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
51 49 50 imbitrrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) )
52 27 51 syldc ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) )
53 52 a1i ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) ) )
54 18 53 tfis2 ⊢ ( 𝑥 ∈ On → ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) )
55 12 54 mpcom ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) )
56 55 3expia ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) )
57 56 com12 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → 𝑥 ⊆ ( 𝐹 ‘ 𝑥 ) ) )
58 4 57 vtoclga ⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → 𝐶 ⊆ ( 𝐹 ‘ 𝐶 ) ) )
59 58 com12 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( 𝐶 ∈ 𝐴 → 𝐶 ⊆ ( 𝐹 ‘ 𝐶 ) ) )
60 59 3impia ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ⊆ ( 𝐹 ‘ 𝐶 ) )