Metamath Proof Explorer

Theorem findcard2d

Description: Deduction version of findcard2 . (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses findcard2d.ch 
|- ( x = (/) -> ( ps <-> ch ) )
findcard2d.th 
|- ( x = y -> ( ps <-> th ) )
findcard2d.ta 
|- ( x = ( y u. { z } ) -> ( ps <-> ta ) )
findcard2d.et 
|- ( x = A -> ( ps <-> et ) )
findcard2d.z 
|- ( ph -> ch )
findcard2d.i 
|- ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( th -> ta ) )
findcard2d.a 
|- ( ph -> A e. Fin )
Assertion findcard2d 
|- ( ph -> et )

Proof

Step Hyp Ref Expression
1 findcard2d.ch 
 |-  ( x = (/) -> ( ps <-> ch ) )
2 findcard2d.th 
 |-  ( x = y -> ( ps <-> th ) )
3 findcard2d.ta 
 |-  ( x = ( y u. { z } ) -> ( ps <-> ta ) )
4 findcard2d.et 
 |-  ( x = A -> ( ps <-> et ) )
5 findcard2d.z 
 |-  ( ph -> ch )
6 findcard2d.i 
 |-  ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( th -> ta ) )
7 findcard2d.a 
 |-  ( ph -> A e. Fin )
8 ssid 
 |-  A C_ A
9 7 adantr 
 |-  ( ( ph /\ A C_ A ) -> A e. Fin )
10 sseq1 
 |-  ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
11 10 anbi2d 
 |-  ( x = (/) -> ( ( ph /\ x C_ A ) <-> ( ph /\ (/) C_ A ) ) )
12 11 1 imbi12d 
 |-  ( x = (/) -> ( ( ( ph /\ x C_ A ) -> ps ) <-> ( ( ph /\ (/) C_ A ) -> ch ) ) )
13 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
14 13 anbi2d 
 |-  ( x = y -> ( ( ph /\ x C_ A ) <-> ( ph /\ y C_ A ) ) )
15 14 2 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x C_ A ) -> ps ) <-> ( ( ph /\ y C_ A ) -> th ) ) )
16 sseq1 
 |-  ( x = ( y u. { z } ) -> ( x C_ A <-> ( y u. { z } ) C_ A ) )
17 16 anbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( ph /\ x C_ A ) <-> ( ph /\ ( y u. { z } ) C_ A ) ) )
18 17 3 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( ph /\ x C_ A ) -> ps ) <-> ( ( ph /\ ( y u. { z } ) C_ A ) -> ta ) ) )
19 sseq1 
 |-  ( x = A -> ( x C_ A <-> A C_ A ) )
20 19 anbi2d 
 |-  ( x = A -> ( ( ph /\ x C_ A ) <-> ( ph /\ A C_ A ) ) )
21 20 4 imbi12d 
 |-  ( x = A -> ( ( ( ph /\ x C_ A ) -> ps ) <-> ( ( ph /\ A C_ A ) -> et ) ) )
22 5 adantr 
 |-  ( ( ph /\ (/) C_ A ) -> ch )
23 simprl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> ph )
24 simprr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> ( y u. { z } ) C_ A )
25 24 unssad 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> y C_ A )
26 23 25 jca 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> ( ph /\ y C_ A ) )
27 id 
 |-  ( ( y u. { z } ) C_ A -> ( y u. { z } ) C_ A )
28 vsnid 
 |-  z e. { z }
29 elun2 
 |-  ( z e. { z } -> z e. ( y u. { z } ) )
30 28 29 mp1i 
 |-  ( ( y u. { z } ) C_ A -> z e. ( y u. { z } ) )
31 27 30 sseldd 
 |-  ( ( y u. { z } ) C_ A -> z e. A )
32 31 ad2antll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> z e. A )
33 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> -. z e. y )
34 32 33 eldifd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> z e. ( A \ y ) )
35 23 25 34 6 syl12anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> ( th -> ta ) )
36 26 35 embantd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( ph /\ ( y u. { z } ) C_ A ) ) -> ( ( ( ph /\ y C_ A ) -> th ) -> ta ) )
37 36 ex 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ph /\ ( y u. { z } ) C_ A ) -> ( ( ( ph /\ y C_ A ) -> th ) -> ta ) ) )
38 37 com23 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ph /\ y C_ A ) -> th ) -> ( ( ph /\ ( y u. { z } ) C_ A ) -> ta ) ) )
39 12 15 18 21 22 38 findcard2s 
 |-  ( A e. Fin -> ( ( ph /\ A C_ A ) -> et ) )
40 9 39 mpcom 
 |-  ( ( ph /\ A C_ A ) -> et )
41 8 40 mpan2 
 |-  ( ph -> et )