Proof of Theorem fin23lem32
Step | Hyp | Ref
| Expression |
1 | | fin23lem.a |
. . . . . . . 8
⊢ 𝑈 =
seq𝜔((𝑖
∈ ω, 𝑢 ∈ V
↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) |
2 | | fin23lem17.f |
. . . . . . . 8
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran
𝑎 ∈ ran 𝑎)} |
3 | | fin23lem.b |
. . . . . . . 8
⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} |
4 | | fin23lem.c |
. . . . . . . 8
⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) |
5 | | fin23lem.d |
. . . . . . . 8
⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) |
6 | | fin23lem.e |
. . . . . . . 8
⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran
𝑈)) ∘ 𝑄)) |
7 | 1, 2, 3, 4, 5, 6 | fin23lem28 9045 |
. . . . . . 7
⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V) |
8 | 7 | ad2antrl 760 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑍:ω–1-1→V) |
9 | | simprl 790 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡:ω–1-1→V) |
10 | | simpl 472 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝐺 ∈ 𝐹) |
11 | | simprr 792 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ∪ ran
𝑡 ⊆ 𝐺) |
12 | 1, 2, 3, 4, 5, 6 | fin23lem31 9048 |
. . . . . . 7
⊢ ((𝑡:ω–1-1→V ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran
𝑡 ⊆ 𝐺) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |
13 | 9, 10, 11, 12 | syl3anc 1318 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |
14 | | f1fn 6015 |
. . . . . . . . . . . 12
⊢ (𝑡:ω–1-1→V → 𝑡 Fn ω) |
15 | | dffn3 5967 |
. . . . . . . . . . . 12
⊢ (𝑡 Fn ω ↔ 𝑡:ω⟶ran 𝑡) |
16 | 14, 15 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝑡:ω–1-1→V → 𝑡:ω⟶ran 𝑡) |
17 | 16 | ad2antrl 760 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡:ω⟶ran 𝑡) |
18 | | sspwuni 4547 |
. . . . . . . . . . . 12
⊢ (ran
𝑡 ⊆ 𝒫 𝐺 ↔ ∪ ran 𝑡 ⊆ 𝐺) |
19 | 18 | biimpri 217 |
. . . . . . . . . . 11
⊢ (∪ ran 𝑡 ⊆ 𝐺 → ran 𝑡 ⊆ 𝒫 𝐺) |
20 | 19 | ad2antll 761 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ran 𝑡 ⊆ 𝒫 𝐺) |
21 | 17, 20 | fssd 5970 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡:ω⟶𝒫 𝐺) |
22 | | pwexg 4776 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ 𝐹 → 𝒫 𝐺 ∈ V) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝒫 𝐺 ∈ V) |
24 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
25 | | f1f 6014 |
. . . . . . . . . . . 12
⊢ (𝑡:ω–1-1→V → 𝑡:ω⟶V) |
26 | | dmfex 7017 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ V ∧ 𝑡:ω⟶V) →
ω ∈ V) |
27 | 24, 25, 26 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝑡:ω–1-1→V → ω ∈ V) |
28 | 27 | ad2antrl 760 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ω ∈ V) |
29 | 23, 28 | elmapd 7758 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↔
𝑡:ω⟶𝒫
𝐺)) |
30 | 21, 29 | mpbird 246 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω)) |
31 | | f1f 6014 |
. . . . . . . . . 10
⊢ (𝑍:ω–1-1→V → 𝑍:ω⟶V) |
32 | 8, 31 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑍:ω⟶V) |
33 | | fex 6394 |
. . . . . . . . 9
⊢ ((𝑍:ω⟶V ∧ ω
∈ V) → 𝑍 ∈
V) |
34 | 32, 28, 33 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑍 ∈ V) |
35 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍) =
(𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍) |
36 | 35 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ∧ 𝑍 ∈ V)
→ ((𝑡 ∈
(𝒫 𝐺
↑𝑚 ω) ↦ 𝑍)‘𝑡) = 𝑍) |
37 | 30, 34, 36 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡) = 𝑍) |
38 | | f1eq1 6009 |
. . . . . . . 8
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) = 𝑍 → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ↔ 𝑍:ω–1-1→V)) |
39 | | rneq 5272 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) = 𝑍 → ran ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡) = ran 𝑍) |
40 | 39 | unieqd 4382 |
. . . . . . . . 9
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) = 𝑍 → ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) = ∪ ran 𝑍) |
41 | 40 | psseq1d 3661 |
. . . . . . . 8
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) = 𝑍 → (∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡 ↔ ∪ ran 𝑍 ⊊ ∪ ran
𝑡)) |
42 | 38, 41 | anbi12d 743 |
. . . . . . 7
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) = 𝑍 → ((((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡) ↔ (𝑍:ω–1-1→V ∧ ∪ ran 𝑍 ⊊ ∪ ran 𝑡))) |
43 | 37, 42 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ((((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡) ↔ (𝑍:ω–1-1→V ∧ ∪ ran 𝑍 ⊊ ∪ ran 𝑡))) |
44 | 8, 13, 43 | mpbir2and 959 |
. . . . 5
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡)) |
45 | 44 | ex 449 |
. . . 4
⊢ (𝐺 ∈ 𝐹 → ((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡))) |
46 | 45 | alrimiv 1842 |
. . 3
⊢ (𝐺 ∈ 𝐹 → ∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡))) |
47 | | ovex 6577 |
. . . . 5
⊢
(𝒫 𝐺
↑𝑚 ω) ∈ V |
48 | 47 | mptex 6390 |
. . . 4
⊢ (𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍) ∈
V |
49 | | nfmpt1 4675 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) |
50 | 49 | nfeq2 2766 |
. . . . 5
⊢
Ⅎ𝑡 𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) |
51 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → (𝑓‘𝑡) = ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡)) |
52 | | f1eq1 6009 |
. . . . . . . 8
⊢ ((𝑓‘𝑡) = ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡) → ((𝑓‘𝑡):ω–1-1→V ↔ ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V)) |
53 | 51, 52 | syl 17 |
. . . . . . 7
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → ((𝑓‘𝑡):ω–1-1→V ↔ ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V)) |
54 | 51 | rneqd 5274 |
. . . . . . . . 9
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → ran (𝑓‘𝑡) = ran ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡)) |
55 | 54 | unieqd 4382 |
. . . . . . . 8
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → ∪ ran (𝑓‘𝑡) = ∪ ran ((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡)) |
56 | 55 | psseq1d 3661 |
. . . . . . 7
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → (∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡 ↔ ∪ ran ((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡) ⊊ ∪ ran
𝑡)) |
57 | 53, 56 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → (((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡) ↔ (((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡))) |
58 | 57 | imbi2d 329 |
. . . . 5
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → (((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)) ↔ ((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡)))) |
59 | 50, 58 | albid 2077 |
. . . 4
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍) → (∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)) ↔ ∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡)))) |
60 | 48, 59 | spcev 3273 |
. . 3
⊢
(∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑𝑚 ω) ↦
𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑𝑚
ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡)) → ∃𝑓∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
61 | 46, 60 | syl 17 |
. 2
⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
62 | | f1eq1 6009 |
. . . . . 6
⊢ (𝑏 = 𝑡 → (𝑏:ω–1-1→V ↔ 𝑡:ω–1-1→V)) |
63 | | rneq 5272 |
. . . . . . . 8
⊢ (𝑏 = 𝑡 → ran 𝑏 = ran 𝑡) |
64 | 63 | unieqd 4382 |
. . . . . . 7
⊢ (𝑏 = 𝑡 → ∪ ran
𝑏 = ∪ ran 𝑡) |
65 | 64 | sseq1d 3595 |
. . . . . 6
⊢ (𝑏 = 𝑡 → (∪ ran
𝑏 ⊆ 𝐺 ↔ ∪ ran
𝑡 ⊆ 𝐺)) |
66 | 62, 65 | anbi12d 743 |
. . . . 5
⊢ (𝑏 = 𝑡 → ((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) ↔ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺))) |
67 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑏 = 𝑡 → (𝑓‘𝑏) = (𝑓‘𝑡)) |
68 | | f1eq1 6009 |
. . . . . . 7
⊢ ((𝑓‘𝑏) = (𝑓‘𝑡) → ((𝑓‘𝑏):ω–1-1→V ↔ (𝑓‘𝑡):ω–1-1→V)) |
69 | 67, 68 | syl 17 |
. . . . . 6
⊢ (𝑏 = 𝑡 → ((𝑓‘𝑏):ω–1-1→V ↔ (𝑓‘𝑡):ω–1-1→V)) |
70 | 67 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑏 = 𝑡 → ran (𝑓‘𝑏) = ran (𝑓‘𝑡)) |
71 | 70 | unieqd 4382 |
. . . . . . 7
⊢ (𝑏 = 𝑡 → ∪ ran
(𝑓‘𝑏) = ∪ ran (𝑓‘𝑡)) |
72 | 71, 64 | psseq12d 3663 |
. . . . . 6
⊢ (𝑏 = 𝑡 → (∪ ran
(𝑓‘𝑏) ⊊ ∪ ran
𝑏 ↔ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)) |
73 | 69, 72 | anbi12d 743 |
. . . . 5
⊢ (𝑏 = 𝑡 → (((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏) ↔ ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
74 | 66, 73 | imbi12d 333 |
. . . 4
⊢ (𝑏 = 𝑡 → (((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏)) ↔ ((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)))) |
75 | 74 | cbvalv 2261 |
. . 3
⊢
(∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏)) ↔ ∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
76 | 75 | exbii 1764 |
. 2
⊢
(∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏)) ↔ ∃𝑓∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
77 | 61, 76 | sylibr 223 |
1
⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏))) |