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