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 sseldi
 |-  ( ( 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 ) )