Step | Hyp | Ref
| Expression |
1 | | domeng 8752 |
. . 3
⊢ (𝑋 ∈ UFL → (𝑌 ≼ 𝑋 ↔ ∃𝑥(𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋))) |
2 | | bren 8743 |
. . . . . . . 8
⊢ (𝑌 ≈ 𝑥 ↔ ∃𝑓 𝑓:𝑌–1-1-onto→𝑥) |
3 | 2 | biimpi 215 |
. . . . . . 7
⊢ (𝑌 ≈ 𝑥 → ∃𝑓 𝑓:𝑌–1-1-onto→𝑥) |
4 | | ssufl 23069 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑥 ⊆ 𝑋) → 𝑥 ∈ UFL) |
5 | | simplr 766 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) → 𝑥 ∈ UFL) |
6 | | filfbas 22999 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ (Fil‘𝑌) → 𝑔 ∈ (fBas‘𝑌)) |
7 | 6 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) → 𝑔 ∈ (fBas‘𝑌)) |
8 | | f1of 6716 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑌–1-1-onto→𝑥 → 𝑓:𝑌⟶𝑥) |
9 | 8 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) → 𝑓:𝑌⟶𝑥) |
10 | | fmfil 23095 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ UFL ∧ 𝑔 ∈ (fBas‘𝑌) ∧ 𝑓:𝑌⟶𝑥) → ((𝑥 FilMap 𝑓)‘𝑔) ∈ (Fil‘𝑥)) |
11 | 5, 7, 9, 10 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) → ((𝑥 FilMap 𝑓)‘𝑔) ∈ (Fil‘𝑥)) |
12 | | ufli 23065 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ UFL ∧ ((𝑥 FilMap 𝑓)‘𝑔) ∈ (Fil‘𝑥)) → ∃𝑦 ∈ (UFil‘𝑥)((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦) |
13 | 5, 11, 12 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) → ∃𝑦 ∈ (UFil‘𝑥)((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦) |
14 | | f1odm 6720 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:𝑌–1-1-onto→𝑥 → dom 𝑓 = 𝑌) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) → dom 𝑓 = 𝑌) |
16 | | vex 3436 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑓 ∈ V |
17 | 16 | dmex 7758 |
. . . . . . . . . . . . . . . . 17
⊢ dom 𝑓 ∈ V |
18 | 15, 17 | eqeltrrdi 2848 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) → 𝑌 ∈ V) |
19 | 18 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑌 ∈ V) |
20 | | simprl 768 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑦 ∈ (UFil‘𝑥)) |
21 | | f1ocnv 6728 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝑌–1-1-onto→𝑥 → ◡𝑓:𝑥–1-1-onto→𝑌) |
22 | 21 | ad3antrrr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ◡𝑓:𝑥–1-1-onto→𝑌) |
23 | | f1of 6716 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑓:𝑥–1-1-onto→𝑌 → ◡𝑓:𝑥⟶𝑌) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ◡𝑓:𝑥⟶𝑌) |
25 | | fmufil 23110 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 ∈ V ∧ 𝑦 ∈ (UFil‘𝑥) ∧ ◡𝑓:𝑥⟶𝑌) → ((𝑌 FilMap ◡𝑓)‘𝑦) ∈ (UFil‘𝑌)) |
26 | 19, 20, 24, 25 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap ◡𝑓)‘𝑦) ∈ (UFil‘𝑌)) |
27 | | f1ococnv1 6745 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:𝑌–1-1-onto→𝑥 → (◡𝑓 ∘ 𝑓) = ( I ↾ 𝑌)) |
28 | 27 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → (◡𝑓 ∘ 𝑓) = ( I ↾ 𝑌)) |
29 | 28 | oveq2d 7291 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → (𝑌 FilMap (◡𝑓 ∘ 𝑓)) = (𝑌 FilMap ( I ↾ 𝑌))) |
30 | 29 | fveq1d 6776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap (◡𝑓 ∘ 𝑓))‘𝑔) = ((𝑌 FilMap ( I ↾ 𝑌))‘𝑔)) |
31 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑥 ∈ UFL) |
32 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑔 ∈ (fBas‘𝑌)) |
33 | 8 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑓:𝑌⟶𝑥) |
34 | | fmco 23112 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑌 ∈ V ∧ 𝑥 ∈ UFL ∧ 𝑔 ∈ (fBas‘𝑌)) ∧ (◡𝑓:𝑥⟶𝑌 ∧ 𝑓:𝑌⟶𝑥)) → ((𝑌 FilMap (◡𝑓 ∘ 𝑓))‘𝑔) = ((𝑌 FilMap ◡𝑓)‘((𝑥 FilMap 𝑓)‘𝑔))) |
35 | 19, 31, 32, 24, 33, 34 | syl32anc 1377 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap (◡𝑓 ∘ 𝑓))‘𝑔) = ((𝑌 FilMap ◡𝑓)‘((𝑥 FilMap 𝑓)‘𝑔))) |
36 | | simplr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑔 ∈ (Fil‘𝑌)) |
37 | | fmid 23111 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ (Fil‘𝑌) → ((𝑌 FilMap ( I ↾ 𝑌))‘𝑔) = 𝑔) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap ( I ↾ 𝑌))‘𝑔) = 𝑔) |
39 | 30, 35, 38 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap ◡𝑓)‘((𝑥 FilMap 𝑓)‘𝑔)) = 𝑔) |
40 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑥 FilMap 𝑓)‘𝑔) ∈ (Fil‘𝑥)) |
41 | | filfbas 22999 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 FilMap 𝑓)‘𝑔) ∈ (Fil‘𝑥) → ((𝑥 FilMap 𝑓)‘𝑔) ∈ (fBas‘𝑥)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑥 FilMap 𝑓)‘𝑔) ∈ (fBas‘𝑥)) |
43 | | ufilfil 23055 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (UFil‘𝑥) → 𝑦 ∈ (Fil‘𝑥)) |
44 | | filfbas 22999 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (Fil‘𝑥) → 𝑦 ∈ (fBas‘𝑥)) |
45 | 20, 43, 44 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑦 ∈ (fBas‘𝑥)) |
46 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦) |
47 | | fmss 23097 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑌 ∈ V ∧ ((𝑥 FilMap 𝑓)‘𝑔) ∈ (fBas‘𝑥) ∧ 𝑦 ∈ (fBas‘𝑥)) ∧ (◡𝑓:𝑥⟶𝑌 ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap ◡𝑓)‘((𝑥 FilMap 𝑓)‘𝑔)) ⊆ ((𝑌 FilMap ◡𝑓)‘𝑦)) |
48 | 19, 42, 45, 24, 46, 47 | syl32anc 1377 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ((𝑌 FilMap ◡𝑓)‘((𝑥 FilMap 𝑓)‘𝑔)) ⊆ ((𝑌 FilMap ◡𝑓)‘𝑦)) |
49 | 39, 48 | eqsstrrd 3960 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → 𝑔 ⊆ ((𝑌 FilMap ◡𝑓)‘𝑦)) |
50 | | sseq2 3947 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = ((𝑌 FilMap ◡𝑓)‘𝑦) → (𝑔 ⊆ 𝑢 ↔ 𝑔 ⊆ ((𝑌 FilMap ◡𝑓)‘𝑦))) |
51 | 50 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢ ((((𝑌 FilMap ◡𝑓)‘𝑦) ∈ (UFil‘𝑌) ∧ 𝑔 ⊆ ((𝑌 FilMap ◡𝑓)‘𝑦)) → ∃𝑢 ∈ (UFil‘𝑌)𝑔 ⊆ 𝑢) |
52 | 26, 49, 51 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) ∧ (𝑦 ∈ (UFil‘𝑥) ∧ ((𝑥 FilMap 𝑓)‘𝑔) ⊆ 𝑦)) → ∃𝑢 ∈ (UFil‘𝑌)𝑔 ⊆ 𝑢) |
53 | 13, 52 | rexlimddv 3220 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) ∧ 𝑔 ∈ (Fil‘𝑌)) → ∃𝑢 ∈ (UFil‘𝑌)𝑔 ⊆ 𝑢) |
54 | 53 | ralrimiva 3103 |
. . . . . . . . . . 11
⊢ ((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) → ∀𝑔 ∈ (Fil‘𝑌)∃𝑢 ∈ (UFil‘𝑌)𝑔 ⊆ 𝑢) |
55 | | isufl 23064 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ V → (𝑌 ∈ UFL ↔ ∀𝑔 ∈ (Fil‘𝑌)∃𝑢 ∈ (UFil‘𝑌)𝑔 ⊆ 𝑢)) |
56 | 18, 55 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) → (𝑌 ∈ UFL ↔ ∀𝑔 ∈ (Fil‘𝑌)∃𝑢 ∈ (UFil‘𝑌)𝑔 ⊆ 𝑢)) |
57 | 54, 56 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) → 𝑌 ∈ UFL) |
58 | 57 | ex 413 |
. . . . . . . . 9
⊢ (𝑓:𝑌–1-1-onto→𝑥 → (𝑥 ∈ UFL → 𝑌 ∈ UFL)) |
59 | 58 | exlimiv 1933 |
. . . . . . . 8
⊢
(∃𝑓 𝑓:𝑌–1-1-onto→𝑥 → (𝑥 ∈ UFL → 𝑌 ∈ UFL)) |
60 | 59 | imp 407 |
. . . . . . 7
⊢
((∃𝑓 𝑓:𝑌–1-1-onto→𝑥 ∧ 𝑥 ∈ UFL) → 𝑌 ∈ UFL) |
61 | 3, 4, 60 | syl2an 596 |
. . . . . 6
⊢ ((𝑌 ≈ 𝑥 ∧ (𝑋 ∈ UFL ∧ 𝑥 ⊆ 𝑋)) → 𝑌 ∈ UFL) |
62 | 61 | an12s 646 |
. . . . 5
⊢ ((𝑋 ∈ UFL ∧ (𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋)) → 𝑌 ∈ UFL) |
63 | 62 | ex 413 |
. . . 4
⊢ (𝑋 ∈ UFL → ((𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋) → 𝑌 ∈ UFL)) |
64 | 63 | exlimdv 1936 |
. . 3
⊢ (𝑋 ∈ UFL → (∃𝑥(𝑌 ≈ 𝑥 ∧ 𝑥 ⊆ 𝑋) → 𝑌 ∈ UFL)) |
65 | 1, 64 | sylbid 239 |
. 2
⊢ (𝑋 ∈ UFL → (𝑌 ≼ 𝑋 → 𝑌 ∈ UFL)) |
66 | 65 | imp 407 |
1
⊢ ((𝑋 ∈ UFL ∧ 𝑌 ≼ 𝑋) → 𝑌 ∈ UFL) |