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

Proof

Step	Hyp	Ref	Expression
1		dominfac.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		omex	⊢ ω ∈ V
21		domtri	⊢ ( ( ω ∈ V ∧ 𝒫 𝑥 ∈ V ) → ( ω ≼ 𝒫 𝑥 ↔ ¬ 𝒫 𝑥 ≺ ω ) )
22	20 12 21	mp2an	⊢ ( ω ≼ 𝒫 𝑥 ↔ ¬ 𝒫 𝑥 ≺ ω )
23		vex	⊢ 𝑥 ∈ V
24		domtri	⊢ ( ( ω ∈ V ∧ 𝑥 ∈ V ) → ( ω ≼ 𝑥 ↔ ¬ 𝑥 ≺ ω ) )
25	20 23 24	mp2an	⊢ ( ω ≼ 𝑥 ↔ ¬ 𝑥 ≺ ω )
26	19 22 25	3imtr4i	⊢ ( ω ≼ 𝒫 𝑥 → ω ≼ 𝑥 )
27	11 13 26	3syl	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ω ≼ 𝑥 )
28	1 8 27	vtocl	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ∪ 𝐴 ) → ω ≼ 𝐴 )

Metamath Proof Explorer

Theorem dominfac

Proof