Theorem fineqvlem

Description: Lemma for fineqv . (Contributed by Mario Carneiro, 20-Jan-2013) (Proof shortened by Stefan O'Rear, 3-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fineqvlem	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ω ≼ 𝒫 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pwexg	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
2	1	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 𝒫 𝐴 ∈ V )
3	2	pwexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 𝒫 𝒫 𝐴 ∈ V )
4		ssrab2	⊢ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ⊆ 𝒫 𝐴
5		elpw2g	⊢ ( 𝒫 𝐴 ∈ V → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ⊆ 𝒫 𝐴 ) )
6	2 5	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ↔ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ⊆ 𝒫 𝐴 ) )
7	4 6	mpbiri	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ∈ 𝒫 𝒫 𝐴 )
8	7	a1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( 𝑏 ∈ ω → { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ∈ 𝒫 𝒫 𝐴 ) )
9		isinf	⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑏 ∈ ω ∃ 𝑒 ( 𝑒 ⊆ 𝐴 ∧ 𝑒 ≈ 𝑏 ) )
10	9	r19.21bi	⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑏 ∈ ω ) → ∃ 𝑒 ( 𝑒 ⊆ 𝐴 ∧ 𝑒 ≈ 𝑏 ) )
11	10	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ∃ 𝑒 ( 𝑒 ⊆ 𝐴 ∧ 𝑒 ≈ 𝑏 ) )
12		velpw	⊢ ( 𝑒 ∈ 𝒫 𝐴 ↔ 𝑒 ⊆ 𝐴 )
13	12	biimpri	⊢ ( 𝑒 ⊆ 𝐴 → 𝑒 ∈ 𝒫 𝐴 )
14	13	anim1i	⊢ ( ( 𝑒 ⊆ 𝐴 ∧ 𝑒 ≈ 𝑏 ) → ( 𝑒 ∈ 𝒫 𝐴 ∧ 𝑒 ≈ 𝑏 ) )
15		breq1	⊢ ( 𝑑 = 𝑒 → ( 𝑑 ≈ 𝑏 ↔ 𝑒 ≈ 𝑏 ) )
16	15	elrab	⊢ ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ↔ ( 𝑒 ∈ 𝒫 𝐴 ∧ 𝑒 ≈ 𝑏 ) )
17	14 16	sylibr	⊢ ( ( 𝑒 ⊆ 𝐴 ∧ 𝑒 ≈ 𝑏 ) → 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } )
18	17	eximi	⊢ ( ∃ 𝑒 ( 𝑒 ⊆ 𝐴 ∧ 𝑒 ≈ 𝑏 ) → ∃ 𝑒 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } )
19	11 18	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ∃ 𝑒 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } )
20		eleq2	⊢ ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ↔ 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ) )
21	20	biimpcd	⊢ ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ) )
22	21	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ) → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ) )
23	16	simprbi	⊢ ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } → 𝑒 ≈ 𝑏 )
24		breq1	⊢ ( 𝑑 = 𝑒 → ( 𝑑 ≈ 𝑐 ↔ 𝑒 ≈ 𝑐 ) )
25	24	elrab	⊢ ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ↔ ( 𝑒 ∈ 𝒫 𝐴 ∧ 𝑒 ≈ 𝑐 ) )
26	25	simprbi	⊢ ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑒 ≈ 𝑐 )
27		ensym	⊢ ( 𝑒 ≈ 𝑏 → 𝑏 ≈ 𝑒 )
28		entr	⊢ ( ( 𝑏 ≈ 𝑒 ∧ 𝑒 ≈ 𝑐 ) → 𝑏 ≈ 𝑐 )
29	27 28	sylan	⊢ ( ( 𝑒 ≈ 𝑏 ∧ 𝑒 ≈ 𝑐 ) → 𝑏 ≈ 𝑐 )
30	23 26 29	syl2an	⊢ ( ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ∧ 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ) → 𝑏 ≈ 𝑐 )
31	30	ex	⊢ ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } → ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑏 ≈ 𝑐 ) )
32	31	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ) → ( 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑏 ≈ 𝑐 ) )
33		nneneq	⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) → ( 𝑏 ≈ 𝑐 ↔ 𝑏 = 𝑐 ) )
34	33	biimpd	⊢ ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) → ( 𝑏 ≈ 𝑐 → 𝑏 = 𝑐 ) )
35	34	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ) → ( 𝑏 ≈ 𝑐 → 𝑏 = 𝑐 ) )
36	22 32 35	3syld	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) ∧ 𝑒 ∈ { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } ) → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑏 = 𝑐 ) )
37	19 36	exlimddv	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } → 𝑏 = 𝑐 ) )
38		breq2	⊢ ( 𝑏 = 𝑐 → ( 𝑑 ≈ 𝑏 ↔ 𝑑 ≈ 𝑐 ) )
39	38	rabbidv	⊢ ( 𝑏 = 𝑐 → { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } )
40	37 39	impbid1	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) ) → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ↔ 𝑏 = 𝑐 ) )
41	40	ex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ( 𝑏 ∈ ω ∧ 𝑐 ∈ ω ) → ( { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑏 } = { 𝑑 ∈ 𝒫 𝐴 ∣ 𝑑 ≈ 𝑐 } ↔ 𝑏 = 𝑐 ) ) )
42	8 41	dom2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( 𝒫 𝒫 𝐴 ∈ V → ω ≼ 𝒫 𝒫 𝐴 ) )
43	3 42	mpd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ω ≼ 𝒫 𝒫 𝐴 )