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