Metamath Proof Explorer


Theorem inawinalem

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

Ref Expression
Assertion inawinalem A On x A 𝒫 x A x A y A x y

Proof

Step Hyp Ref Expression
1 sdomdom 𝒫 x A 𝒫 x A
2 ondomen A On 𝒫 x A 𝒫 x dom card
3 isnum2 𝒫 x dom card y On y 𝒫 x
4 2 3 sylib A On 𝒫 x A y On y 𝒫 x
5 1 4 sylan2 A On 𝒫 x A y On y 𝒫 x
6 ensdomtr y 𝒫 x 𝒫 x A y A
7 6 ad2ant2l y On y 𝒫 x A On 𝒫 x A y A
8 sdomel y On A On y A y A
9 8 ad2ant2r y On y 𝒫 x A On 𝒫 x A y A y A
10 7 9 mpd y On y 𝒫 x A On 𝒫 x A y A
11 vex x V
12 11 canth2 x 𝒫 x
13 ensym y 𝒫 x 𝒫 x y
14 sdomentr x 𝒫 x 𝒫 x y x y
15 12 13 14 sylancr y 𝒫 x x y
16 15 ad2antlr y On y 𝒫 x A On 𝒫 x A x y
17 10 16 jca y On y 𝒫 x A On 𝒫 x A y A x y
18 17 expcom A On 𝒫 x A y On y 𝒫 x y A x y
19 18 reximdv2 A On 𝒫 x A y On y 𝒫 x y A x y
20 5 19 mpd A On 𝒫 x A y A x y
21 20 ex A On 𝒫 x A y A x y
22 21 ralimdv A On x A 𝒫 x A x A y A x y