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