Metamath Proof Explorer


Theorem zorn2lem1

Description: Lemma for zorn2 . (Contributed by NM, 3-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses zorn2lem.3 F = recs f V ι v C | u C ¬ u w v
zorn2lem.4 C = z A | g ran f g R z
zorn2lem.5 D = z A | g F x g R z
Assertion zorn2lem1 x On w We A D F x D

Proof

Step Hyp Ref Expression
1 zorn2lem.3 F = recs f V ι v C | u C ¬ u w v
2 zorn2lem.4 C = z A | g ran f g R z
3 zorn2lem.5 D = z A | g F x g R z
4 1 tfr2 x On F x = f V ι v C | u C ¬ u w v F x
5 4 adantr x On w We A D F x = f V ι v C | u C ¬ u w v F x
6 1 tfr1 F Fn On
7 fnfun F Fn On Fun F
8 6 7 ax-mp Fun F
9 vex x V
10 resfunexg Fun F x V F x V
11 8 9 10 mp2an F x V
12 rneq f = F x ran f = ran F x
13 df-ima F x = ran F x
14 12 13 eqtr4di f = F x ran f = F x
15 14 eleq2d f = F x g ran f g F x
16 15 imbi1d f = F x g ran f g R z g F x g R z
17 16 ralbidv2 f = F x g ran f g R z g F x g R z
18 17 rabbidv f = F x z A | g ran f g R z = z A | g F x g R z
19 18 2 3 3eqtr4g f = F x C = D
20 19 eleq2d f = F x u C u D
21 20 imbi1d f = F x u C ¬ u w v u D ¬ u w v
22 21 ralbidv2 f = F x u C ¬ u w v u D ¬ u w v
23 19 22 riotaeqbidv f = F x ι v C | u C ¬ u w v = ι v D | u D ¬ u w v
24 eqid f V ι v C | u C ¬ u w v = f V ι v C | u C ¬ u w v
25 riotaex ι v D | u D ¬ u w v V
26 23 24 25 fvmpt F x V f V ι v C | u C ¬ u w v F x = ι v D | u D ¬ u w v
27 11 26 ax-mp f V ι v C | u C ¬ u w v F x = ι v D | u D ¬ u w v
28 5 27 eqtrdi x On w We A D F x = ι v D | u D ¬ u w v
29 simprl x On w We A D w We A
30 weso w We A w Or A
31 30 ad2antrl x On w We A D w Or A
32 vex w V
33 soex w Or A w V A V
34 31 32 33 sylancl x On w We A D A V
35 3 34 rabexd x On w We A D D V
36 3 ssrab3 D A
37 36 a1i x On w We A D D A
38 simprr x On w We A D D
39 wereu w We A D V D A D ∃! v D u D ¬ u w v
40 29 35 37 38 39 syl13anc x On w We A D ∃! v D u D ¬ u w v
41 riotacl ∃! v D u D ¬ u w v ι v D | u D ¬ u w v D
42 40 41 syl x On w We A D ι v D | u D ¬ u w v D
43 28 42 eqeltrd x On w We A D F x D