Proof of Theorem fin23lem32
Step | Hyp | Ref
| Expression |
1 | | fin23lem.a |
. . . . . . . 8
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) |
2 | | fin23lem17.f |
. . . . . . . 8
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘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 9840 |
. . . . . . 7
⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V) |
8 | 7 | ad2antrl 728 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑍:ω–1-1→V) |
9 | | simprl 771 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡:ω–1-1→V) |
10 | | simpl 486 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝐺 ∈ 𝐹) |
11 | | simprr 773 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ∪ ran
𝑡 ⊆ 𝐺) |
12 | 1, 2, 3, 4, 5, 6 | fin23lem31 9843 |
. . . . . . 7
⊢ ((𝑡:ω–1-1→V ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran
𝑡 ⊆ 𝐺) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |
13 | 9, 10, 11, 12 | syl3anc 1372 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ∪ ran
𝑍 ⊊ ∪ ran 𝑡) |
14 | | f1fn 6575 |
. . . . . . . . . . . 12
⊢ (𝑡:ω–1-1→V → 𝑡 Fn ω) |
15 | | dffn3 6517 |
. . . . . . . . . . . 12
⊢ (𝑡 Fn ω ↔ 𝑡:ω⟶ran 𝑡) |
16 | 14, 15 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝑡:ω–1-1→V → 𝑡:ω⟶ran 𝑡) |
17 | 16 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡:ω⟶ran 𝑡) |
18 | | sspwuni 4985 |
. . . . . . . . . . . 12
⊢ (ran
𝑡 ⊆ 𝒫 𝐺 ↔ ∪ ran 𝑡 ⊆ 𝐺) |
19 | 18 | biimpri 231 |
. . . . . . . . . . 11
⊢ (∪ ran 𝑡 ⊆ 𝐺 → ran 𝑡 ⊆ 𝒫 𝐺) |
20 | 19 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ran 𝑡 ⊆ 𝒫 𝐺) |
21 | 17, 20 | fssd 6522 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡:ω⟶𝒫 𝐺) |
22 | | pwexg 5245 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ 𝐹 → 𝒫 𝐺 ∈ V) |
23 | 22 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝒫 𝐺 ∈ V) |
24 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
25 | | f1f 6574 |
. . . . . . . . . . . 12
⊢ (𝑡:ω–1-1→V → 𝑡:ω⟶V) |
26 | | dmfex 7638 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ V ∧ 𝑡:ω⟶V) →
ω ∈ V) |
27 | 24, 25, 26 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝑡:ω–1-1→V → ω ∈ V) |
28 | 27 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ω ∈ V) |
29 | 23, 28 | elmapd 8451 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↔ 𝑡:ω⟶𝒫 𝐺)) |
30 | 21, 29 | mpbird 260 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑡 ∈ (𝒫 𝐺 ↑m
ω)) |
31 | | f1f 6574 |
. . . . . . . . . 10
⊢ (𝑍:ω–1-1→V → 𝑍:ω⟶V) |
32 | 8, 31 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑍:ω⟶V) |
33 | 32, 28 | fexd 7000 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → 𝑍 ∈ V) |
34 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍) = (𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍) |
35 | 34 | fvmpt2 6786 |
. . . . . . . 8
⊢ ((𝑡 ∈ (𝒫 𝐺 ↑m ω)
∧ 𝑍 ∈ V) →
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = 𝑍) |
36 | 30, 33, 35 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡) = 𝑍) |
37 | | f1eq1 6569 |
. . . . . . . 8
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = 𝑍 → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ↔ 𝑍:ω–1-1→V)) |
38 | | rneq 5779 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = 𝑍 → ran ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡) = ran 𝑍) |
39 | 38 | unieqd 4810 |
. . . . . . . . 9
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = 𝑍 → ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = ∪
ran 𝑍) |
40 | 39 | psseq1d 3983 |
. . . . . . . 8
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = 𝑍 → (∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡 ↔ ∪ ran
𝑍 ⊊ ∪ ran 𝑡)) |
41 | 37, 40 | anbi12d 634 |
. . . . . . 7
⊢ (((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) = 𝑍 → ((((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡) ↔ (𝑍:ω–1-1→V ∧ ∪ ran 𝑍 ⊊ ∪ ran 𝑡))) |
42 | 36, 41 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → ((((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡) ↔ (𝑍:ω–1-1→V ∧ ∪ ran 𝑍 ⊊ ∪ ran 𝑡))) |
43 | 8, 13, 42 | mpbir2and 713 |
. . . . 5
⊢ ((𝐺 ∈ 𝐹 ∧ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺)) → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡)) |
44 | 43 | ex 416 |
. . . 4
⊢ (𝐺 ∈ 𝐹 → ((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡))) |
45 | 44 | alrimiv 1934 |
. . 3
⊢ (𝐺 ∈ 𝐹 → ∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡))) |
46 | | ovex 7203 |
. . . . 5
⊢
(𝒫 𝐺
↑m ω) ∈ V |
47 | 46 | mptex 6996 |
. . . 4
⊢ (𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍) ∈
V |
48 | | nfmpt1 5128 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) |
49 | 48 | nfeq2 2916 |
. . . . 5
⊢
Ⅎ𝑡 𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) |
50 | | fveq1 6673 |
. . . . . . . 8
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → (𝑓‘𝑡) = ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡)) |
51 | | f1eq1 6569 |
. . . . . . . 8
⊢ ((𝑓‘𝑡) = ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡) → ((𝑓‘𝑡):ω–1-1→V ↔ ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V)) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → ((𝑓‘𝑡):ω–1-1→V ↔ ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V)) |
53 | 50 | rneqd 5781 |
. . . . . . . . 9
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → ran (𝑓‘𝑡) = ran ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡)) |
54 | 53 | unieqd 4810 |
. . . . . . . 8
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → ∪ ran (𝑓‘𝑡) = ∪ ran ((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡)) |
55 | 54 | psseq1d 3983 |
. . . . . . 7
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → (∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡 ↔ ∪ ran ((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡) ⊊ ∪ ran
𝑡)) |
56 | 52, 55 | anbi12d 634 |
. . . . . 6
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → (((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡) ↔ (((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡))) |
57 | 56 | imbi2d 344 |
. . . . 5
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → (((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)) ↔ ((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡)))) |
58 | 49, 57 | albid 2224 |
. . . 4
⊢ (𝑓 = (𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍) → (∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)) ↔ ∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡)))) |
59 | 47, 58 | spcev 3510 |
. . 3
⊢
(∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → (((𝑡 ∈ (𝒫 𝐺 ↑m ω) ↦ 𝑍)‘𝑡):ω–1-1→V ∧ ∪ ran
((𝑡 ∈ (𝒫 𝐺 ↑m ω)
↦ 𝑍)‘𝑡) ⊊ ∪ ran 𝑡)) → ∃𝑓∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
60 | 45, 59 | syl 17 |
. 2
⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
61 | | f1eq1 6569 |
. . . . . 6
⊢ (𝑏 = 𝑡 → (𝑏:ω–1-1→V ↔ 𝑡:ω–1-1→V)) |
62 | | rneq 5779 |
. . . . . . . 8
⊢ (𝑏 = 𝑡 → ran 𝑏 = ran 𝑡) |
63 | 62 | unieqd 4810 |
. . . . . . 7
⊢ (𝑏 = 𝑡 → ∪ ran
𝑏 = ∪ ran 𝑡) |
64 | 63 | sseq1d 3908 |
. . . . . 6
⊢ (𝑏 = 𝑡 → (∪ ran
𝑏 ⊆ 𝐺 ↔ ∪ ran
𝑡 ⊆ 𝐺)) |
65 | 61, 64 | anbi12d 634 |
. . . . 5
⊢ (𝑏 = 𝑡 → ((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) ↔ (𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺))) |
66 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑏 = 𝑡 → (𝑓‘𝑏) = (𝑓‘𝑡)) |
67 | | f1eq1 6569 |
. . . . . . 7
⊢ ((𝑓‘𝑏) = (𝑓‘𝑡) → ((𝑓‘𝑏):ω–1-1→V ↔ (𝑓‘𝑡):ω–1-1→V)) |
68 | 66, 67 | syl 17 |
. . . . . 6
⊢ (𝑏 = 𝑡 → ((𝑓‘𝑏):ω–1-1→V ↔ (𝑓‘𝑡):ω–1-1→V)) |
69 | 66 | rneqd 5781 |
. . . . . . . 8
⊢ (𝑏 = 𝑡 → ran (𝑓‘𝑏) = ran (𝑓‘𝑡)) |
70 | 69 | unieqd 4810 |
. . . . . . 7
⊢ (𝑏 = 𝑡 → ∪ ran
(𝑓‘𝑏) = ∪ ran (𝑓‘𝑡)) |
71 | 70, 63 | psseq12d 3985 |
. . . . . 6
⊢ (𝑏 = 𝑡 → (∪ ran
(𝑓‘𝑏) ⊊ ∪ ran
𝑏 ↔ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)) |
72 | 68, 71 | anbi12d 634 |
. . . . 5
⊢ (𝑏 = 𝑡 → (((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏) ↔ ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
73 | 65, 72 | imbi12d 348 |
. . . 4
⊢ (𝑏 = 𝑡 → (((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏)) ↔ ((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡)))) |
74 | 73 | cbvalvw 2048 |
. . 3
⊢
(∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏)) ↔ ∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
75 | 74 | exbii 1854 |
. 2
⊢
(∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏)) ↔ ∃𝑓∀𝑡((𝑡:ω–1-1→V ∧ ∪ ran 𝑡 ⊆ 𝐺) → ((𝑓‘𝑡):ω–1-1→V ∧ ∪ ran (𝑓‘𝑡) ⊊ ∪ ran
𝑡))) |
76 | 60, 75 | sylibr 237 |
1
⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran
𝑏))) |