Metamath Proof Explorer


Theorem hartogslem1

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

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 hartogslem1 dom F 𝒫 A × A Fun F A V ran F = x On | x A

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 dmeqi dom F = dom 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
4 dmopab dom 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 = 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
5 3 4 eqtri dom 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
6 simp3 dom r A I dom r r r dom r × dom r r dom r × dom r
7 simp1 dom r A I dom r r r dom r × dom r dom r A
8 xpss12 dom r A dom r A dom r × dom r A × A
9 7 7 8 syl2anc dom r A I dom r r r dom r × dom r dom r × dom r A × A
10 6 9 sstrd dom r A I dom r r r dom r × dom r r A × A
11 velpw r 𝒫 A × A r A × A
12 10 11 sylibr dom r A I dom r r r dom r × dom r r 𝒫 A × A
13 12 ad2antrr dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r r 𝒫 A × A
14 13 exlimiv 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 r 𝒫 A × A
15 14 abssi 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 𝒫 A × A
16 5 15 eqsstri dom F 𝒫 A × A
17 funopab4 Fun 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
18 1 funeqi Fun F Fun 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
19 17 18 mpbir Fun F
20 1 rneqi ran F = ran 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
21 rnopab ran 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 = y | r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
22 20 21 eqtri ran F = y | r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
23 breq1 x = y x A y A
24 23 elrab y x On | x A y On y A
25 f1f f : y 1-1 A f : y A
26 25 adantl y On f : y 1-1 A f : y A
27 26 frnd y On f : y 1-1 A ran f A
28 resss I ran f I
29 ssun2 I R I
30 28 29 sstri I ran f R I
31 idssxp I ran f ran f × ran f
32 30 31 ssini I ran f R I ran f × ran f
33 32 a1i y On f : y 1-1 A I ran f R I ran f × ran f
34 inss2 R I ran f × ran f ran f × ran f
35 34 a1i y On f : y 1-1 A R I ran f × ran f ran f × ran f
36 27 33 35 3jca y On f : y 1-1 A ran f A I ran f R I ran f × ran f R I ran f × ran f ran f × ran f
37 eloni y On Ord y
38 ordwe Ord y E We y
39 37 38 syl y On E We y
40 39 adantr y On f : y 1-1 A E We y
41 f1f1orn f : y 1-1 A f : y 1-1 onto ran f
42 41 adantl y On f : y 1-1 A f : y 1-1 onto ran f
43 f1oiso f : y 1-1 onto ran f R = s t | w y z y s = f w t = f z w E z f Isom E , R y ran f
44 42 2 43 sylancl y On f : y 1-1 A f Isom E , R y ran f
45 isores2 f Isom E , R y ran f f Isom E , R ran f × ran f y ran f
46 44 45 sylib y On f : y 1-1 A f Isom E , R ran f × ran f y ran f
47 isowe f Isom E , R ran f × ran f y ran f E We y R ran f × ran f We ran f
48 46 47 syl y On f : y 1-1 A E We y R ran f × ran f We ran f
49 40 48 mpbid y On f : y 1-1 A R ran f × ran f We ran f
50 weso R ran f × ran f We ran f R ran f × ran f Or ran f
51 49 50 syl y On f : y 1-1 A R ran f × ran f Or ran f
52 inss2 R ran f × ran f ran f × ran f
53 52 brel x R ran f × ran f x x ran f x ran f
54 53 simpld x R ran f × ran f x x ran f
55 sonr R ran f × ran f Or ran f x ran f ¬ x R ran f × ran f x
56 51 54 55 syl2an y On f : y 1-1 A x R ran f × ran f x ¬ x R ran f × ran f x
57 56 pm2.01da y On f : y 1-1 A ¬ x R ran f × ran f x
58 57 alrimiv y On f : y 1-1 A x ¬ x R ran f × ran f x
59 intirr R ran f × ran f I = x ¬ x R ran f × ran f x
60 58 59 sylibr y On f : y 1-1 A R ran f × ran f I =
61 disj3 R ran f × ran f I = R ran f × ran f = R ran f × ran f I
62 60 61 sylib y On f : y 1-1 A R ran f × ran f = R ran f × ran f I
63 weeq1 R ran f × ran f = R ran f × ran f I R ran f × ran f We ran f R ran f × ran f I We ran f
64 62 63 syl y On f : y 1-1 A R ran f × ran f We ran f R ran f × ran f I We ran f
65 49 64 mpbid y On f : y 1-1 A R ran f × ran f I We ran f
66 37 adantr y On f : y 1-1 A Ord y
67 isoeq3 R ran f × ran f = R ran f × ran f I f Isom E , R ran f × ran f y ran f f Isom E , R ran f × ran f I y ran f
68 62 67 syl y On f : y 1-1 A f Isom E , R ran f × ran f y ran f f Isom E , R ran f × ran f I y ran f
69 46 68 mpbid y On f : y 1-1 A f Isom E , R ran f × ran f I y ran f
70 vex f V
71 70 rnex ran f V
72 exse ran f V R ran f × ran f I Se ran f
73 71 72 ax-mp R ran f × ran f I Se ran f
74 eqid OrdIso R ran f × ran f I ran f = OrdIso R ran f × ran f I ran f
75 74 oieu R ran f × ran f I We ran f R ran f × ran f I Se ran f Ord y f Isom E , R ran f × ran f I y ran f y = dom OrdIso R ran f × ran f I ran f f = OrdIso R ran f × ran f I ran f
76 65 73 75 sylancl y On f : y 1-1 A Ord y f Isom E , R ran f × ran f I y ran f y = dom OrdIso R ran f × ran f I ran f f = OrdIso R ran f × ran f I ran f
77 66 69 76 mpbi2and y On f : y 1-1 A y = dom OrdIso R ran f × ran f I ran f f = OrdIso R ran f × ran f I ran f
78 77 simpld y On f : y 1-1 A y = dom OrdIso R ran f × ran f I ran f
79 71 71 xpex ran f × ran f V
80 79 inex2 R I ran f × ran f V
81 sseq1 r = R I ran f × ran f r ran f × ran f R I ran f × ran f ran f × ran f
82 34 81 mpbiri r = R I ran f × ran f r ran f × ran f
83 dmss r ran f × ran f dom r dom ran f × ran f
84 82 83 syl r = R I ran f × ran f dom r dom ran f × ran f
85 dmxpid dom ran f × ran f = ran f
86 84 85 sseqtrdi r = R I ran f × ran f dom r ran f
87 dmresi dom I ran f = ran f
88 sseq2 r = R I ran f × ran f I ran f r I ran f R I ran f × ran f
89 32 88 mpbiri r = R I ran f × ran f I ran f r
90 dmss I ran f r dom I ran f dom r
91 89 90 syl r = R I ran f × ran f dom I ran f dom r
92 87 91 eqsstrrid r = R I ran f × ran f ran f dom r
93 86 92 eqssd r = R I ran f × ran f dom r = ran f
94 93 sseq1d r = R I ran f × ran f dom r A ran f A
95 93 reseq2d r = R I ran f × ran f I dom r = I ran f
96 id r = R I ran f × ran f r = R I ran f × ran f
97 95 96 sseq12d r = R I ran f × ran f I dom r r I ran f R I ran f × ran f
98 93 sqxpeqd r = R I ran f × ran f dom r × dom r = ran f × ran f
99 96 98 sseq12d r = R I ran f × ran f r dom r × dom r R I ran f × ran f ran f × ran f
100 94 97 99 3anbi123d r = R I ran f × ran f dom r A I dom r r r dom r × dom r ran f A I ran f R I ran f × ran f R I ran f × ran f ran f × ran f
101 difeq1 r = R I ran f × ran f r I = R I ran f × ran f I
102 difun2 R I I = R I
103 102 ineq1i R I I ran f × ran f = R I ran f × ran f
104 indif1 R I I ran f × ran f = R I ran f × ran f I
105 indif1 R I ran f × ran f = R ran f × ran f I
106 103 104 105 3eqtr3i R I ran f × ran f I = R ran f × ran f I
107 101 106 eqtrdi r = R I ran f × ran f r I = R ran f × ran f I
108 107 93 weeq12d r = R I ran f × ran f r I We dom r R ran f × ran f I We ran f
109 100 108 anbi12d r = R I ran f × ran f dom r A I dom r r r dom r × dom r r I We dom r ran f A I ran f R I ran f × ran f R I ran f × ran f ran f × ran f R ran f × ran f I We ran f
110 oieq1 r I = R ran f × ran f I OrdIso r I dom r = OrdIso R ran f × ran f I dom r
111 107 110 syl r = R I ran f × ran f OrdIso r I dom r = OrdIso R ran f × ran f I dom r
112 oieq2 dom r = ran f OrdIso R ran f × ran f I dom r = OrdIso R ran f × ran f I ran f
113 93 112 syl r = R I ran f × ran f OrdIso R ran f × ran f I dom r = OrdIso R ran f × ran f I ran f
114 111 113 eqtrd r = R I ran f × ran f OrdIso r I dom r = OrdIso R ran f × ran f I ran f
115 114 dmeqd r = R I ran f × ran f dom OrdIso r I dom r = dom OrdIso R ran f × ran f I ran f
116 115 eqeq2d r = R I ran f × ran f y = dom OrdIso r I dom r y = dom OrdIso R ran f × ran f I ran f
117 109 116 anbi12d r = R I ran f × ran f dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r ran f A I ran f R I ran f × ran f R I ran f × ran f ran f × ran f R ran f × ran f I We ran f y = dom OrdIso R ran f × ran f I ran f
118 80 117 spcev ran f A I ran f R I ran f × ran f R I ran f × ran f ran f × ran f R ran f × ran f I We ran f y = dom OrdIso R ran f × ran f I ran f r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
119 36 65 78 118 syl21anc y On f : y 1-1 A r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
120 119 ex y On f : y 1-1 A r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
121 120 exlimdv y On f f : y 1-1 A r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
122 brdomi y A f f : y 1-1 A
123 121 122 impel y On y A r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
124 simpr dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y = dom OrdIso r I dom r
125 vex r V
126 125 dmex dom r V
127 eqid OrdIso r I dom r = OrdIso r I dom r
128 127 oion dom r V dom OrdIso r I dom r On
129 126 128 ax-mp dom OrdIso r I dom r On
130 124 129 eqeltrdi dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y On
131 130 adantl A V dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y On
132 simplr dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r r I We dom r
133 127 oien dom r V r I We dom r dom OrdIso r I dom r dom r
134 126 132 133 sylancr dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r dom OrdIso r I dom r dom r
135 124 134 eqbrtrd dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y dom r
136 ssdomg A V dom r A dom r A
137 simpll1 dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r dom r A
138 136 137 impel A V dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r dom r A
139 endomtr y dom r dom r A y A
140 135 138 139 syl2an2 A V dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y A
141 131 140 jca A V dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y On y A
142 141 ex A V dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y On y A
143 142 exlimdv A V r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r y On y A
144 123 143 impbid2 A V y On y A r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
145 24 144 bitrid A V y x On | x A r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
146 145 eqabdv A V x On | x A = y | r dom r A I dom r r r dom r × dom r r I We dom r y = dom OrdIso r I dom r
147 22 146 eqtr4id A V ran F = x On | x A
148 16 19 147 3pm3.2i dom F 𝒫 A × A Fun F A V ran F = x On | x A