Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝐶 → 𝑥 = 𝐶) |
2 | | fveq2 6801 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶)) |
3 | 1, 2 | sseq12d 3960 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝐶 ⊆ (𝐹‘𝐶))) |
4 | 3 | imbi2d 342 |
. . . 4
⊢ (𝑥 = 𝐶 → (((𝐹 Fn 𝐴 ∧ Smo 𝐹) → 𝑥 ⊆ (𝐹‘𝑥)) ↔ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → 𝐶 ⊆ (𝐹‘𝐶)))) |
5 | | smodm2 8214 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) |
6 | 5 | 3adant3 1132 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → Ord 𝐴) |
7 | | simp3 1138 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
8 | | ordelord 6300 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) |
9 | 6, 7, 8 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → Ord 𝑥) |
10 | | vex 3442 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
11 | 10 | elon 6287 |
. . . . . . . 8
⊢ (𝑥 ∈ On ↔ Ord 𝑥) |
12 | 9, 11 | sylibr 234 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
13 | | eleq1w 2819 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
14 | 13 | 3anbi3d 1442 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) ↔ (𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴))) |
15 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
16 | | fveq2 6801 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
17 | 15, 16 | sseq12d 3960 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝐹‘𝑥) ↔ 𝑦 ⊆ (𝐹‘𝑦))) |
18 | 14, 17 | imbi12d 346 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ (𝐹‘𝑥)) ↔ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ (𝐹‘𝑦)))) |
19 | | simpl1 1191 |
. . . . . . . . . . . 12
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝐹 Fn 𝐴) |
20 | | simpl2 1192 |
. . . . . . . . . . . 12
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → Smo 𝐹) |
21 | | ordtr1 6321 |
. . . . . . . . . . . . . . 15
⊢ (Ord
𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐴)) |
22 | 21 | expcomd 418 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝐴 → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴))) |
23 | 6, 7, 22 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴)) |
24 | 23 | imp 408 |
. . . . . . . . . . . 12
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴) |
25 | | pm2.27 42 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ (𝐹‘𝑦)) → 𝑦 ⊆ (𝐹‘𝑦))) |
26 | 19, 20, 24, 25 | syl3anc 1371 |
. . . . . . . . . . 11
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ (𝐹‘𝑦)) → 𝑦 ⊆ (𝐹‘𝑦))) |
27 | 26 | ralimdva 3161 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ (𝐹‘𝑦)) → ∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐹‘𝑦))) |
28 | 5 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → Ord 𝐴) |
29 | | simp31 1209 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → 𝑥 ∈ 𝐴) |
30 | 28, 29, 8 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → Ord 𝑥) |
31 | | simp32 1210 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → 𝑦 ∈ 𝑥) |
32 | | ordelord 6300 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Ord
𝑥 ∧ 𝑦 ∈ 𝑥) → Ord 𝑦) |
33 | 30, 31, 32 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → Ord 𝑦) |
34 | | smofvon2 8215 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Smo
𝐹 → (𝐹‘𝑥) ∈ On) |
35 | 34 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → (𝐹‘𝑥) ∈ On) |
36 | | eloni 6288 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) ∈ On → Ord (𝐹‘𝑥)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → Ord (𝐹‘𝑥)) |
38 | | simp33 1211 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → 𝑦 ⊆ (𝐹‘𝑦)) |
39 | | smoel2 8222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
40 | 39 | 3adantr3 1171 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
41 | 40 | 3impa 1110 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
42 | | ordtr2 6322 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Ord
𝑦 ∧ Ord (𝐹‘𝑥)) → ((𝑦 ⊆ (𝐹‘𝑦) ∧ (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → 𝑦 ∈ (𝐹‘𝑥))) |
43 | 42 | imp 408 |
. . . . . . . . . . . . . . . . 17
⊢ (((Ord
𝑦 ∧ Ord (𝐹‘𝑥)) ∧ (𝑦 ⊆ (𝐹‘𝑦) ∧ (𝐹‘𝑦) ∈ (𝐹‘𝑥))) → 𝑦 ∈ (𝐹‘𝑥)) |
44 | 33, 37, 38, 41, 43 | syl22anc 837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦))) → 𝑦 ∈ (𝐹‘𝑥)) |
45 | 44 | 3expia 1121 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ (𝐹‘𝑦)) → 𝑦 ∈ (𝐹‘𝑥))) |
46 | 45 | 3expd 1353 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → (𝑦 ⊆ (𝐹‘𝑦) → 𝑦 ∈ (𝐹‘𝑥))))) |
47 | 46 | 3impia 1117 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝑥 → (𝑦 ⊆ (𝐹‘𝑦) → 𝑦 ∈ (𝐹‘𝑥)))) |
48 | 47 | imp 408 |
. . . . . . . . . . . 12
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑦 ⊆ (𝐹‘𝑦) → 𝑦 ∈ (𝐹‘𝑥))) |
49 | 48 | ralimdva 3161 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐹‘𝑦) → ∀𝑦 ∈ 𝑥 𝑦 ∈ (𝐹‘𝑥))) |
50 | | dfss3 3915 |
. . . . . . . . . . 11
⊢ (𝑥 ⊆ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝑥 𝑦 ∈ (𝐹‘𝑥)) |
51 | 49, 50 | syl6ibr 253 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 𝑦 ⊆ (𝐹‘𝑦) → 𝑥 ⊆ (𝐹‘𝑥))) |
52 | 27, 51 | syldc 48 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑥 ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ (𝐹‘𝑦)) → ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ (𝐹‘𝑥))) |
53 | 52 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ (𝐹‘𝑦)) → ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ (𝐹‘𝑥)))) |
54 | 18, 53 | tfis2 7732 |
. . . . . . 7
⊢ (𝑥 ∈ On → ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ (𝐹‘𝑥))) |
55 | 12, 54 | mpcom 38 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ (𝐹‘𝑥)) |
56 | 55 | 3expia 1121 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → (𝑥 ∈ 𝐴 → 𝑥 ⊆ (𝐹‘𝑥))) |
57 | 56 | com12 32 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → 𝑥 ⊆ (𝐹‘𝑥))) |
58 | 4, 57 | vtoclga 3519 |
. . 3
⊢ (𝐶 ∈ 𝐴 → ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → 𝐶 ⊆ (𝐹‘𝐶))) |
59 | 58 | com12 32 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → (𝐶 ∈ 𝐴 → 𝐶 ⊆ (𝐹‘𝐶))) |
60 | 59 | 3impia 1117 |
1
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹 ∧ 𝐶 ∈ 𝐴) → 𝐶 ⊆ (𝐹‘𝐶)) |