This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ω ≼ 𝒫 𝒫 𝐴 )