Metamath Proof Explorer

Theorem dominfac

Description: A nonempty set that is a subset of its union is infinite. This version is proved from ax-ac . See dominf for a version proved from ax-cc . (Contributed by NM, 25-Mar-2007)

Ref Expression
Hypothesis dominfac.1 ⊢A∈V
Assertion dominfac ⊢A≠∅∧A⊆⋃A→ω≼A

Proof

Step Hyp Ref Expression
1 dominfac.1 ⊢A∈V
2 neeq1 ⊢x=A→x≠∅↔A≠∅
3 id ⊢x=A→x=A
4 unieq ⊢x=A→⋃x=⋃A
5 3 4 sseq12d ⊢x=A→x⊆⋃x↔A⊆⋃A
6 2 5 anbi12d ⊢x=A→x≠∅∧x⊆⋃x↔A≠∅∧A⊆⋃A
7 breq2 ⊢x=A→ω≼x↔ω≼A
8 6 7 imbi12d ⊢x=A→x≠∅∧x⊆⋃x→ω≼x↔A≠∅∧A⊆⋃A→ω≼A
9 eqid ⊢y∈V⟼w∈x|w∩x⊆y=y∈V⟼w∈x|w∩x⊆y
10 eqid ⊢rec⁡y∈V⟼w∈x|w∩x⊆y∅↾ω=rec⁡y∈V⟼w∈x|w∩x⊆y∅↾ω
11 9 10 1 1 inf3lem6 ⊢x≠∅∧x⊆⋃x→rec⁡y∈V⟼w∈x|w∩x⊆y∅↾ω:ω⟶1-1𝒫x
12 vpwex ⊢𝒫x∈V
13 12 f1dom ⊢rec⁡y∈V⟼w∈x|w∩x⊆y∅↾ω:ω⟶1-1𝒫x→ω≼𝒫x
14 pwfi ⊢x∈Fin↔𝒫x∈Fin
15 14 biimpi ⊢x∈Fin→𝒫x∈Fin
16 isfinite ⊢x∈Fin↔x≺ω
17 isfinite ⊢𝒫x∈Fin↔𝒫x≺ω
18 15 16 17 3imtr3i ⊢x≺ω→𝒫x≺ω
19 18 con3i ⊢¬𝒫x≺ω→¬x≺ω
20 omex ⊢ω∈V
21 domtri ⊢ω∈V∧𝒫x∈V→ω≼𝒫x↔¬𝒫x≺ω
22 20 12 21 mp2an ⊢ω≼𝒫x↔¬𝒫x≺ω
23 vex ⊢x∈V
24 domtri ⊢ω∈V∧x∈V→ω≼x↔¬x≺ω
25 20 23 24 mp2an ⊢ω≼x↔¬x≺ω
26 19 22 25 3imtr4i ⊢ω≼𝒫x→ω≼x
27 11 13 26 3syl ⊢x≠∅∧x⊆⋃x→ω≼x
28 1 8 27 vtocl ⊢A≠∅∧A⊆⋃A→ω≼A