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 → ( ∀ 𝑥𝐴 𝒫 𝑥𝐴 → ∀ 𝑥𝐴𝑦𝐴 𝑥𝑦 ) )