Metamath Proof Explorer

Theorem dominf

Description: A nonempty set that is a subset of its union is infinite. This version is proved from ax-cc . See dominfac for a version proved from ax-ac . The axiom of Regularity is used for this proof, via inf3lem6 , and its use is necessary: otherwise the set A = { A } or A = { (/) , A } (where the second example even has nonempty well-founded part) provides a counterexample. (Contributed by Mario Carneiro, 9-Feb-2013)

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

Proof

Step Hyp Ref Expression
1 dominf.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 12 domtriom ⊢ω≼𝒫x↔¬𝒫x≺ω
21 vex ⊢x∈V
22 21 domtriom ⊢ω≼x↔¬x≺ω
23 19 20 22 3imtr4i ⊢ω≼𝒫x→ω≼x
24 11 13 23 3syl ⊢x≠∅∧x⊆⋃x→ω≼x
25 1 8 24 vtocl ⊢A≠∅∧A⊆⋃A→ω≼A