Step | Hyp | Ref
| Expression |
1 | | stoweidlem27.4 |
. . . 4
⊢ (𝜑 → 𝑌 Fn ran 𝐺) |
2 | | stoweidlem27.5 |
. . . 4
⊢ (𝜑 → ran 𝐺 ∈ V) |
3 | | fnex 6386 |
. . . 4
⊢ ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V) |
4 | 1, 2, 3 | syl2anc 691 |
. . 3
⊢ (𝜑 → 𝑌 ∈ V) |
5 | | stoweidlem27.7 |
. . . . 5
⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran
𝐺) |
6 | | f1ofn 6051 |
. . . . 5
⊢ (𝐹:(1...𝑀)–1-1-onto→ran
𝐺 → 𝐹 Fn (1...𝑀)) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 Fn (1...𝑀)) |
8 | | ovex 6577 |
. . . 4
⊢
(1...𝑀) ∈
V |
9 | | fnex 6386 |
. . . 4
⊢ ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V) |
10 | 7, 8, 9 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
11 | | coexg 7010 |
. . 3
⊢ ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌 ∘ 𝐹) ∈ V) |
12 | 4, 10, 11 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑌 ∘ 𝐹) ∈ V) |
13 | | stoweidlem27.3 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
14 | | f1of 6050 |
. . . . . 6
⊢ (𝐹:(1...𝑀)–1-1-onto→ran
𝐺 → 𝐹:(1...𝑀)⟶ran 𝐺) |
15 | 5, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:(1...𝑀)⟶ran 𝐺) |
16 | | fnfco 5982 |
. . . . 5
⊢ ((𝑌 Fn ran 𝐺 ∧ 𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌 ∘ 𝐹) Fn (1...𝑀)) |
17 | 1, 15, 16 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑌 ∘ 𝐹) Fn (1...𝑀)) |
18 | | rncoss 5307 |
. . . . 5
⊢ ran
(𝑌 ∘ 𝐹) ⊆ ran 𝑌 |
19 | | fvelrnb 6153 |
. . . . . . . . . . 11
⊢ (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)) |
20 | 1, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)) |
21 | 20 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘) |
22 | | stoweidlem27.10 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤𝜑 |
23 | | stoweidlem27.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
24 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
25 | 23, 24 | nfcxfr 2749 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑤𝐺 |
26 | 25 | nfrn 5289 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤ran
𝐺 |
27 | 26 | nfcri 2745 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤 𝑙 ∈ ran 𝐺 |
28 | 22, 27 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑤(𝜑 ∧ 𝑙 ∈ ran 𝐺) |
29 | | stoweidlem27.6 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) |
30 | 29 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑙) |
31 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
32 | 30, 31 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
33 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎℎ(𝑌‘𝑙) |
34 | | stoweidlem27.11 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎℎ𝑄 |
35 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)} |
36 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑌‘𝑙) → (ℎ‘𝑡) = ((𝑌‘𝑙)‘𝑡)) |
37 | 36 | breq2d 4595 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑌‘𝑙) → (0 < (ℎ‘𝑡) ↔ 0 < ((𝑌‘𝑙)‘𝑡))) |
38 | 37 | rabbidv 3164 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑌‘𝑙) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}) |
39 | 38 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑌‘𝑙) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})) |
40 | 33, 34, 35, 39 | elrabf 3329 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})) |
41 | 32, 40 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})) |
42 | 41 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑄) |
43 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺) |
44 | 23 | elrnmpt 5293 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
46 | 43, 45 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
47 | 28, 42, 46 | r19.29af 3058 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄) |
48 | 47 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄) |
49 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ ((𝑌‘𝑙) = 𝑘 → ((𝑌‘𝑙) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄)) |
50 | 48, 49 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌‘𝑙) = 𝑘 → 𝑘 ∈ 𝑄)) |
51 | 50 | reximdva 3000 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘 → ∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄)) |
52 | 21, 51 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄) |
53 | | idd 24 |
. . . . . . . . . 10
⊢ (𝑙 ∈ ran 𝐺 → (𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄)) |
54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (𝑙 ∈ ran 𝐺 → (𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))) |
55 | 54 | rexlimdv 3012 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄)) |
56 | 52, 55 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → 𝑘 ∈ 𝑄) |
57 | 56 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄)) |
58 | 57 | ssrdv 3574 |
. . . . 5
⊢ (𝜑 → ran 𝑌 ⊆ 𝑄) |
59 | 18, 58 | syl5ss 3579 |
. . . 4
⊢ (𝜑 → ran (𝑌 ∘ 𝐹) ⊆ 𝑄) |
60 | | df-f 5808 |
. . . 4
⊢ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌 ∘ 𝐹) Fn (1...𝑀) ∧ ran (𝑌 ∘ 𝐹) ⊆ 𝑄)) |
61 | 17, 59, 60 | sylanbrc 695 |
. . 3
⊢ (𝜑 → (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄) |
62 | | stoweidlem27.9 |
. . . 4
⊢
Ⅎ𝑡𝜑 |
63 | | stoweidlem27.8 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋) |
64 | 63 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝑡 ∈ ∪ 𝑋) |
65 | | eluni 4375 |
. . . . . . . 8
⊢ (𝑡 ∈ ∪ 𝑋
↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) |
66 | 64, 65 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) |
67 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑡 ∈ (𝑇 ∖ 𝑈) |
68 | 22, 67 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑤(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) |
69 | 23 | funmpt2 5841 |
. . . . . . . . . . . . . 14
⊢ Fun 𝐺 |
70 | 23 | dmeqi 5247 |
. . . . . . . . . . . . . . . . 17
⊢ dom 𝐺 = dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
71 | | stoweidlem27.2 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑄 ∈ V) |
72 | 34 | rabexgf 38206 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
74 | 73 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
75 | 74 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑤 ∈ 𝑋 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)) |
76 | 22, 75 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) |
77 | | dmmptg 5549 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋) |
79 | 70, 78 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐺 = 𝑋) |
80 | 79 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋)) |
81 | 80 | biimpar 501 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ dom 𝐺) |
82 | | fvelrn 6260 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐺 ∧ 𝑤 ∈ dom 𝐺) → (𝐺‘𝑤) ∈ ran 𝐺) |
83 | 69, 81, 82 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) ∈ ran 𝐺) |
84 | 83 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (𝐺‘𝑤) ∈ ran 𝐺) |
85 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺) |
86 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝑖 ∈ (1...𝑀)) |
87 | | fvco3 6185 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖))) |
88 | 85, 86, 87 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖))) |
89 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑖) = (𝐺‘𝑤) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤))) |
90 | 89 | ad2antll 761 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤))) |
91 | 88, 90 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐺‘𝑤))) |
92 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = (𝐺‘𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺‘𝑤) ∈ ran 𝐺)) |
93 | 92 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = (𝐺‘𝑤) → ((𝜑 ∧ 𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺))) |
94 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘𝑙) ∈ (𝐺‘𝑤))) |
95 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = (𝐺‘𝑤) → (𝑌‘𝑙) = (𝑌‘(𝐺‘𝑤))) |
96 | 95 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ (𝐺‘𝑤) ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))) |
97 | 94, 96 | bitrd 267 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))) |
98 | 93, 97 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = (𝐺‘𝑤) → (((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))) |
99 | 98, 29 | vtoclg 3239 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))) |
100 | 99 | anabsi7 856 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)) |
102 | 91, 101 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) |
103 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(1...𝑀)–1-1-onto→ran
𝐺 → 𝐹:(1...𝑀)–onto→ran 𝐺) |
104 | | forn 6031 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺) |
105 | 5, 103, 104 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝐹 = ran 𝐺) |
106 | 105 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ (𝐺‘𝑤) ∈ ran 𝐺)) |
107 | 106 | biimpar 501 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝐺‘𝑤) ∈ ran 𝐹) |
108 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀)) |
109 | | fvelrnb 6153 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn (1...𝑀) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))) |
111 | 107, 110 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)) |
112 | 102, 111 | reximddv 3001 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) |
113 | 84, 112 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) |
114 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ 𝑤) |
115 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋) |
116 | 23 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ 𝑋 ∧ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
117 | 115, 74, 116 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
118 | 117 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) ↔ ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})) |
119 | 118 | biimpa 500 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
120 | 119 | adantlrl 752 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) |
121 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎℎ((𝑌 ∘ 𝐹)‘𝑖) |
122 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} |
123 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (ℎ‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
124 | 123 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (0 < (ℎ‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
125 | 124 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}) |
126 | 125 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})) |
127 | 121, 34, 122, 126 | elrabf 3329 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})) |
128 | 120, 127 | sylib 207 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})) |
129 | 128 | simprd 478 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}) |
130 | 114, 129 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}) |
131 | | rabid 3095 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
132 | 130, 131 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
133 | 132 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
134 | 133 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
135 | 134 | reximdv 2999 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
136 | 113, 135 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
137 | 136 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
138 | 137 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
139 | 68, 138 | eximd 2072 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
140 | 66, 139 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
141 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡) |
142 | | idd 24 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
143 | 68, 141, 142 | exlimd 2074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (∃𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
144 | 140, 143 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
145 | 144 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
146 | 62, 145 | ralrimi 2940 |
. . 3
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
147 | 13, 61, 146 | jca32 556 |
. 2
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))) |
148 | | feq1 5939 |
. . . . 5
⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄)) |
149 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞‘𝑖) = ((𝑌 ∘ 𝐹)‘𝑖)) |
150 | 149 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞‘𝑖)‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)) |
151 | 150 | breq2d 4595 |
. . . . . . 7
⊢ (𝑞 = (𝑌 ∘ 𝐹) → (0 < ((𝑞‘𝑖)‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
152 | 151 | rexbidv 3034 |
. . . . . 6
⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
153 | 152 | ralbidv 2969 |
. . . . 5
⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) |
154 | 148, 153 | anbi12d 743 |
. . . 4
⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)) ↔ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))) |
155 | 154 | anbi2d 736 |
. . 3
⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))) |
156 | 155 | spcegv 3267 |
. 2
⊢ ((𝑌 ∘ 𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))) |
157 | 12, 147, 156 | sylc 63 |
1
⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)))) |