Metamath Proof Explorer

Theorem aomclem2

Description: Lemma for dfac11 . Successor case 2, a choice function for subsets of ( R1dom z ) . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses aomclem2.b 
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
aomclem2.c 
|- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
aomclem2.on 
|- ( ph -> dom z e. On )
aomclem2.su 
|- ( ph -> dom z = suc U. dom z )
aomclem2.we 
|- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
aomclem2.a 
|- ( ph -> A e. On )
aomclem2.za 
|- ( ph -> dom z C_ A )
aomclem2.y 
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
Assertion aomclem2 
|- ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) )

Proof

Step Hyp Ref Expression
1 aomclem2.b 
 |-  B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
2 aomclem2.c 
 |-  C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
3 aomclem2.on 
 |-  ( ph -> dom z e. On )
4 aomclem2.su 
 |-  ( ph -> dom z = suc U. dom z )
5 aomclem2.we 
 |-  ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
6 aomclem2.a 
 |-  ( ph -> A e. On )
7 aomclem2.za 
 |-  ( ph -> dom z C_ A )
8 aomclem2.y 
 |-  ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
9 vex 
 |-  a e. _V
10 3 6 jca 
 |-  ( ph -> ( dom z e. On /\ A e. On ) )
11 r1ord3 
 |-  ( ( dom z e. On /\ A e. On ) -> ( dom z C_ A -> ( R1 ` dom z ) C_ ( R1 ` A ) ) )
12 10 7 11 sylc 
 |-  ( ph -> ( R1 ` dom z ) C_ ( R1 ` A ) )
13 12 sspwd 
 |-  ( ph -> ~P ( R1 ` dom z ) C_ ~P ( R1 ` A ) )
14 13 sseld 
 |-  ( ph -> ( a e. ~P ( R1 ` dom z ) -> a e. ~P ( R1 ` A ) ) )
15 rsp 
 |-  ( A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) -> ( a e. ~P ( R1 ` A ) -> ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) )
16 8 14 15 sylsyld 
 |-  ( ph -> ( a e. ~P ( R1 ` dom z ) -> ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) ) )
17 16 3imp 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) )
18 17 eldifad 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) e. ( ~P a i^i Fin ) )
19 inss1 
 |-  ( ~P a i^i Fin ) C_ ~P a
20 19 sseli 
 |-  ( ( y ` a ) e. ( ~P a i^i Fin ) -> ( y ` a ) e. ~P a )
21 20 elpwid 
 |-  ( ( y ` a ) e. ( ~P a i^i Fin ) -> ( y ` a ) C_ a )
22 18 21 syl 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) C_ a )
23 1 3 4 5 aomclem1 
 |-  ( ph -> B Or ( R1 ` dom z ) )
24 23 3ad2ant1 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> B Or ( R1 ` dom z ) )
25 inss2 
 |-  ( ~P a i^i Fin ) C_ Fin
26 25 18 sselid 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) e. Fin )
27 eldifsni 
 |-  ( ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) -> ( y ` a ) =/= (/) )
28 17 27 syl 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) =/= (/) )
29 elpwi 
 |-  ( a e. ~P ( R1 ` dom z ) -> a C_ ( R1 ` dom z ) )
30 29 3ad2ant2 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> a C_ ( R1 ` dom z ) )
31 22 30 sstrd 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( y ` a ) C_ ( R1 ` dom z ) )
32 fisupcl 
 |-  ( ( B Or ( R1 ` dom z ) /\ ( ( y ` a ) e. Fin /\ ( y ` a ) =/= (/) /\ ( y ` a ) C_ ( R1 ` dom z ) ) ) -> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. ( y ` a ) )
33 24 26 28 31 32 syl13anc 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. ( y ` a ) )
34 22 33 sseldd 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. a )
35 2 fvmpt2 
 |-  ( ( a e. _V /\ sup ( ( y ` a ) , ( R1 ` dom z ) , B ) e. a ) -> ( C ` a ) = sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
36 9 34 35 sylancr 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( C ` a ) = sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
37 36 34 eqeltrd 
 |-  ( ( ph /\ a e. ~P ( R1 ` dom z ) /\ a =/= (/) ) -> ( C ` a ) e. a )
38 37 3exp 
 |-  ( ph -> ( a e. ~P ( R1 ` dom z ) -> ( a =/= (/) -> ( C ` a ) e. a ) ) )
39 38 ralrimiv 
 |-  ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) )