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	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ∪ 𝐴 ) → ω ≼ 𝐴 )