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

Metamath Proof Explorer

Theorem inawinalem

Description: Lemma for inawina . (Contributed by Mario Carneiro, 8-Jun-2014)

Ref Expression
Assertion inawinalem ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝒫 𝑥 ≺ 𝐴 → 𝒫 𝑥 ≼ 𝐴 )
2 ondomen ⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≼ 𝐴 ) → 𝒫 𝑥 ∈ dom card )
3 isnum2 ⊢ ( 𝒫 𝑥 ∈ dom card ↔ ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 )
4 2 3 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≼ 𝐴 ) → ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 )
5 1 4 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 )
6 ensdomtr ⊢ ( ( 𝑦 ≈ 𝒫 𝑥 ∧ 𝒫 𝑥 ≺ 𝐴 ) → 𝑦 ≺ 𝐴 )
7 6 ad2ant2l ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → 𝑦 ≺ 𝐴 )
8 sdomel ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ≺ 𝐴 → 𝑦 ∈ 𝐴 ) )
9 8 ad2ant2r ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → ( 𝑦 ≺ 𝐴 → 𝑦 ∈ 𝐴 ) )
10 7 9 mpd ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
11 vex ⊢ 𝑥 ∈ V
12 11 canth2 ⊢ 𝑥 ≺ 𝒫 𝑥
13 ensym ⊢ ( 𝑦 ≈ 𝒫 𝑥 → 𝒫 𝑥 ≈ 𝑦 )
14 sdomentr ⊢ ( ( 𝑥 ≺ 𝒫 𝑥 ∧ 𝒫 𝑥 ≈ 𝑦 ) → 𝑥 ≺ 𝑦 )
15 12 13 14 sylancr ⊢ ( 𝑦 ≈ 𝒫 𝑥 → 𝑥 ≺ 𝑦 )
16 15 ad2antlr ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → 𝑥 ≺ 𝑦 )
17 10 16 jca ⊢ ( ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) ∧ ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≺ 𝑦 ) )
18 17 expcom ⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ( ( 𝑦 ∈ On ∧ 𝑦 ≈ 𝒫 𝑥 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≺ 𝑦 ) ) )
19 18 reximdv2 ⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ( ∃ 𝑦 ∈ On 𝑦 ≈ 𝒫 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
20 5 19 mpd ⊢ ( ( 𝐴 ∈ On ∧ 𝒫 𝑥 ≺ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 )
21 20 ex ⊢ ( 𝐴 ∈ On → ( 𝒫 𝑥 ≺ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
22 21 ralimdv ⊢ ( 𝐴 ∈ On → ( ∀ 𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )