Metamath Proof Explorer


Theorem hartogslem2

Description: Lemma for hartogs . (Contributed by Mario Carneiro, 14-Jan-2013)

Ref Expression
Hypotheses hartogslem.2 F = r y | dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
hartogslem.3 R = s t | w y z y s = f w t = f z w E z
Assertion hartogslem2 A V x On | x A V

Proof

Step Hyp Ref Expression
1 hartogslem.2 F = r y | dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
2 hartogslem.3 R = s t | w y z y s = f w t = f z w E z
3 1 2 hartogslem1 dom F 𝒫 A × A Fun F A V ran F = x On | x A
4 3 simp3i A V ran F = x On | x A
5 3 simp2i Fun F
6 3 simp1i dom F 𝒫 A × A
7 sqxpexg A V A × A V
8 7 pwexd A V 𝒫 A × A V
9 ssexg dom F 𝒫 A × A 𝒫 A × A V dom F V
10 6 8 9 sylancr A V dom F V
11 funex Fun F dom F V F V
12 5 10 11 sylancr A V F V
13 rnexg F V ran F V
14 12 13 syl A V ran F V
15 4 14 eqeltrrd A V x On | x A V