Metamath Proof Explorer

Theorem mreexexd

Description: Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if F and G are disjoint from H , ( F u. H ) is independent, F is contained in the closure of ( G u. H ) , and either F or G is finite, then there is a subset q of G equinumerous to F such that ( q u. H ) is independent. This implies the case of Proposition 4.2.1 in FaureFrolicher p. 86 where either ( A \ B ) or ( B \ A ) is finite. The theorem is proven by induction using mreexexlem3d for the base case and mreexexlem4d for the induction step. (Contributed by David Moews, 1-May-2017) Remove dependencies on ax-rep and ax-ac2 . (Revised by Brendan Leahy, 2-Jun-2021)

Ref Expression
Hypotheses mreexexlem2d.1 
|- ( ph -> A e. ( Moore ` X ) )
mreexexlem2d.2 
|- N = ( mrCls ` A )
mreexexlem2d.3 
|- I = ( mrInd ` A )
mreexexlem2d.4 
|- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
mreexexlem2d.5 
|- ( ph -> F C_ ( X \ H ) )
mreexexlem2d.6 
|- ( ph -> G C_ ( X \ H ) )
mreexexlem2d.7 
|- ( ph -> F C_ ( N ` ( G u. H ) ) )
mreexexlem2d.8 
|- ( ph -> ( F u. H ) e. I )
mreexexd.9 
|- ( ph -> ( F e. Fin \/ G e. Fin ) )
Assertion mreexexd 
|- ( ph -> E. q e. ~P G ( F ~~ q /\ ( q u. H ) e. I ) )

Proof

Step Hyp Ref Expression
1 mreexexlem2d.1 
 |-  ( ph -> A e. ( Moore ` X ) )
2 mreexexlem2d.2 
 |-  N = ( mrCls ` A )
3 mreexexlem2d.3 
 |-  I = ( mrInd ` A )
4 mreexexlem2d.4 
 |-  ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
5 mreexexlem2d.5 
 |-  ( ph -> F C_ ( X \ H ) )
6 mreexexlem2d.6 
 |-  ( ph -> G C_ ( X \ H ) )
7 mreexexlem2d.7 
 |-  ( ph -> F C_ ( N ` ( G u. H ) ) )
8 mreexexlem2d.8 
 |-  ( ph -> ( F u. H ) e. I )
9 mreexexd.9 
 |-  ( ph -> ( F e. Fin \/ G e. Fin ) )
10 1 elfvexd 
 |-  ( ph -> X e. _V )
11 exmid 
 |-  ( F e. Fin \/ -. F e. Fin )
12 ficardid 
 |-  ( F e. Fin -> ( card ` F ) ~~ F )
13 12 ensymd 
 |-  ( F e. Fin -> F ~~ ( card ` F ) )
14 iftrue 
 |-  ( F e. Fin -> if ( F e. Fin , ( card ` F ) , ( card ` G ) ) = ( card ` F ) )
15 13 14 breqtrrd 
 |-  ( F e. Fin -> F ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) )
16 15 a1i 
 |-  ( ph -> ( F e. Fin -> F ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) )
17 9 orcanai 
 |-  ( ( ph /\ -. F e. Fin ) -> G e. Fin )
18 ficardid 
 |-  ( G e. Fin -> ( card ` G ) ~~ G )
19 18 ensymd 
 |-  ( G e. Fin -> G ~~ ( card ` G ) )
20 17 19 syl 
 |-  ( ( ph /\ -. F e. Fin ) -> G ~~ ( card ` G ) )
21 iffalse 
 |-  ( -. F e. Fin -> if ( F e. Fin , ( card ` F ) , ( card ` G ) ) = ( card ` G ) )
22 21 adantl 
 |-  ( ( ph /\ -. F e. Fin ) -> if ( F e. Fin , ( card ` F ) , ( card ` G ) ) = ( card ` G ) )
23 20 22 breqtrrd 
 |-  ( ( ph /\ -. F e. Fin ) -> G ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) )
24 23 ex 
 |-  ( ph -> ( -. F e. Fin -> G ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) )
25 16 24 orim12d 
 |-  ( ph -> ( ( F e. Fin \/ -. F e. Fin ) -> ( F ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ G ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) ) )
26 11 25 mpi 
 |-  ( ph -> ( F ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ G ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) )
27 ficardom 
 |-  ( F e. Fin -> ( card ` F ) e. _om )
28 27 adantl 
 |-  ( ( ph /\ F e. Fin ) -> ( card ` F ) e. _om )
29 ficardom 
 |-  ( G e. Fin -> ( card ` G ) e. _om )
30 17 29 syl 
 |-  ( ( ph /\ -. F e. Fin ) -> ( card ` G ) e. _om )
31 28 30 ifclda 
 |-  ( ph -> if ( F e. Fin , ( card ` F ) , ( card ` G ) ) e. _om )
32 breq2 
 |-  ( l = (/) -> ( f ~~ l <-> f ~~ (/) ) )
33 breq2 
 |-  ( l = (/) -> ( g ~~ l <-> g ~~ (/) ) )
34 32 33 orbi12d 
 |-  ( l = (/) -> ( ( f ~~ l \/ g ~~ l ) <-> ( f ~~ (/) \/ g ~~ (/) ) ) )
35 34 3anbi1d 
 |-  ( l = (/) -> ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) <-> ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) )
36 35 imbi1d 
 |-  ( l = (/) -> ( ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
37 36 2ralbidv 
 |-  ( l = (/) -> ( A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
38 37 albidv 
 |-  ( l = (/) -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
39 38 imbi2d 
 |-  ( l = (/) -> ( ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) <-> ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
40 breq2 
 |-  ( l = k -> ( f ~~ l <-> f ~~ k ) )
41 breq2 
 |-  ( l = k -> ( g ~~ l <-> g ~~ k ) )
42 40 41 orbi12d 
 |-  ( l = k -> ( ( f ~~ l \/ g ~~ l ) <-> ( f ~~ k \/ g ~~ k ) ) )
43 42 3anbi1d 
 |-  ( l = k -> ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) <-> ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) )
44 43 imbi1d 
 |-  ( l = k -> ( ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
45 44 2ralbidv 
 |-  ( l = k -> ( A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
46 45 albidv 
 |-  ( l = k -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
47 46 imbi2d 
 |-  ( l = k -> ( ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) <-> ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
48 breq2 
 |-  ( l = suc k -> ( f ~~ l <-> f ~~ suc k ) )
49 breq2 
 |-  ( l = suc k -> ( g ~~ l <-> g ~~ suc k ) )
50 48 49 orbi12d 
 |-  ( l = suc k -> ( ( f ~~ l \/ g ~~ l ) <-> ( f ~~ suc k \/ g ~~ suc k ) ) )
51 50 3anbi1d 
 |-  ( l = suc k -> ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) <-> ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) )
52 51 imbi1d 
 |-  ( l = suc k -> ( ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
53 52 2ralbidv 
 |-  ( l = suc k -> ( A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
54 53 albidv 
 |-  ( l = suc k -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
55 54 imbi2d 
 |-  ( l = suc k -> ( ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) <-> ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
56 breq2 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( f ~~ l <-> f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) )
57 breq2 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( g ~~ l <-> g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) )
58 56 57 orbi12d 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( ( f ~~ l \/ g ~~ l ) <-> ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) ) )
59 58 3anbi1d 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) <-> ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) )
60 59 imbi1d 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> ( ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
61 60 2ralbidv 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
62 61 albidv 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) <-> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
63 62 imbi2d 
 |-  ( l = if ( F e. Fin , ( card ` F ) , ( card ` G ) ) -> ( ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ l \/ g ~~ l ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) <-> ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
64 1 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> A e. ( Moore ` X ) )
65 4 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
66 simplrl 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> f e. ~P ( X \ h ) )
67 66 elpwid 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> f C_ ( X \ h ) )
68 simplrr 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> g e. ~P ( X \ h ) )
69 68 elpwid 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> g C_ ( X \ h ) )
70 simpr2 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> f C_ ( N ` ( g u. h ) ) )
71 simpr3 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> ( f u. h ) e. I )
72 simpr1 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> ( f ~~ (/) \/ g ~~ (/) ) )
73 en0 
 |-  ( f ~~ (/) <-> f = (/) )
74 en0 
 |-  ( g ~~ (/) <-> g = (/) )
75 73 74 orbi12i 
 |-  ( ( f ~~ (/) \/ g ~~ (/) ) <-> ( f = (/) \/ g = (/) ) )
76 72 75 sylib 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> ( f = (/) \/ g = (/) ) )
77 64 2 3 65 67 69 70 71 76 mreexexlem3d 
 |-  ( ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
78 77 ex 
 |-  ( ( ph /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) -> ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
79 78 ralrimivva 
 |-  ( ph -> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
80 79 alrimiv 
 |-  ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ (/) \/ g ~~ (/) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
81 nfv 
 |-  F/ h ph
82 nfv 
 |-  F/ h k e. _om
83 nfa1 
 |-  F/ h A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
84 81 82 83 nf3an 
 |-  F/ h ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
85 nfv 
 |-  F/ f ph
86 nfv 
 |-  F/ f k e. _om
87 nfra1 
 |-  F/ f A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
88 87 nfal 
 |-  F/ f A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
89 85 86 88 nf3an 
 |-  F/ f ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
90 nfv 
 |-  F/ g ph
91 nfv 
 |-  F/ g k e. _om
92 nfra2w 
 |-  F/ g A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
93 92 nfal 
 |-  F/ g A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
94 90 91 93 nf3an 
 |-  F/ g ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
95 nfv 
 |-  F/ g f e. ~P ( X \ h )
96 94 95 nfan 
 |-  F/ g ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ f e. ~P ( X \ h ) )
97 1 3ad2ant1 
 |-  ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) -> A e. ( Moore ` X ) )
98 97 ad2antrr 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> A e. ( Moore ` X ) )
99 4 3ad2ant1 
 |-  ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
100 99 ad2antrr 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
101 simplrl 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> f e. ~P ( X \ h ) )
102 101 elpwid 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> f C_ ( X \ h ) )
103 simplrr 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> g e. ~P ( X \ h ) )
104 103 elpwid 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> g C_ ( X \ h ) )
105 simpr2 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> f C_ ( N ` ( g u. h ) ) )
106 simpr3 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> ( f u. h ) e. I )
107 simpll2 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> k e. _om )
108 simpll3 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
109 simpr1 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> ( f ~~ suc k \/ g ~~ suc k ) )
110 98 2 3 100 102 104 105 106 107 108 109 mreexexlem4d 
 |-  ( ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) /\ ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) )
111 110 ex 
 |-  ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ ( f e. ~P ( X \ h ) /\ g e. ~P ( X \ h ) ) ) -> ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
112 111 expr 
 |-  ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ f e. ~P ( X \ h ) ) -> ( g e. ~P ( X \ h ) -> ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
113 96 112 ralrimi 
 |-  ( ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) /\ f e. ~P ( X \ h ) ) -> A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
114 113 ex 
 |-  ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) -> ( f e. ~P ( X \ h ) -> A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
115 89 114 ralrimi 
 |-  ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) -> A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
116 84 115 alrimi 
 |-  ( ( ph /\ k e. _om /\ A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
117 116 3exp 
 |-  ( ph -> ( k e. _om -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
118 117 com12 
 |-  ( k e. _om -> ( ph -> ( A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
119 118 a2d 
 |-  ( k e. _om -> ( ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ k \/ g ~~ k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) -> ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ suc k \/ g ~~ suc k ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) ) )
120 39 47 55 63 80 119 finds 
 |-  ( if ( F e. Fin , ( card ` F ) , ( card ` G ) ) e. _om -> ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) ) )
121 31 120 mpcom 
 |-  ( ph -> A. h A. f e. ~P ( X \ h ) A. g e. ~P ( X \ h ) ( ( ( f ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) \/ g ~~ if ( F e. Fin , ( card ` F ) , ( card ` G ) ) ) /\ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> E. i e. ~P g ( f ~~ i /\ ( i u. h ) e. I ) ) )
122 10 5 6 7 8 26 121 mreexexlemd 
 |-  ( ph -> E. q e. ~P G ( F ~~ q /\ ( q u. H ) e. I ) )