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 𝐴 ∈ V
Assertion dominf ( ( 𝐴 ≠ ∅ ∧ 𝐴 𝐴 ) → ω ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 dominf.1 𝐴 ∈ V
2 neeq1 ( 𝑥 = 𝐴 → ( 𝑥 ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
3 id ( 𝑥 = 𝐴𝑥 = 𝐴 )
4 unieq ( 𝑥 = 𝐴 𝑥 = 𝐴 )
5 3 4 sseq12d ( 𝑥 = 𝐴 → ( 𝑥 𝑥𝐴 𝐴 ) )
6 2 5 anbi12d ( 𝑥 = 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 𝐴 ) ) )
7 breq2 ( 𝑥 = 𝐴 → ( ω ≼ 𝑥 ↔ ω ≼ 𝐴 ) )
8 6 7 imbi12d ( 𝑥 = 𝐴 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ω ≼ 𝑥 ) ↔ ( ( 𝐴 ≠ ∅ ∧ 𝐴 𝐴 ) → ω ≼ 𝐴 ) ) )
9 eqid ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } ) = ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } )
10 eqid ( rec ( ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω )
11 9 10 1 1 inf3lem6 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( rec ( ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) : ω –1-1→ 𝒫 𝑥 )
12 vpwex 𝒫 𝑥 ∈ V
13 12 f1dom ( ( rec ( ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) : ω –1-1→ 𝒫 𝑥 → ω ≼ 𝒫 𝑥 )
14 pwfi ( 𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Fin )
15 14 biimpi ( 𝑥 ∈ Fin → 𝒫 𝑥 ∈ Fin )
16 isfinite ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω )
17 isfinite ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 𝑥 ≺ ω )
18 15 16 17 3imtr3i ( 𝑥 ≺ ω → 𝒫 𝑥 ≺ ω )
19 18 con3i ( ¬ 𝒫 𝑥 ≺ ω → ¬ 𝑥 ≺ ω )
20 12 domtriom ( ω ≼ 𝒫 𝑥 ↔ ¬ 𝒫 𝑥 ≺ ω )
21 vex 𝑥 ∈ V
22 21 domtriom ( ω ≼ 𝑥 ↔ ¬ 𝑥 ≺ ω )
23 19 20 22 3imtr4i ( ω ≼ 𝒫 𝑥 → ω ≼ 𝑥 )
24 11 13 23 3syl ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ω ≼ 𝑥 )
25 1 8 24 vtocl ( ( 𝐴 ≠ ∅ ∧ 𝐴 𝐴 ) → ω ≼ 𝐴 )