marypha1lem

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015)

		Ref	Expression
	Assertion	marypha1lem	\|- ( A e. Fin -> ( b e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. e e. ~P c e : A -1-1-> _V ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq1	\|- ( a = f -> ( a X. b ) = ( f X. b ) )
2	1	pweqd	\|- ( a = f -> ~P ( a X. b ) = ~P ( f X. b ) )
3		pweq	\|- ( a = f -> ~P a = ~P f )
4	3	raleqdv	\|- ( a = f -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P f d ~<_ ( c " d ) ) )
5		f1eq2	\|- ( a = f -> ( e : a -1-1-> _V <-> e : f -1-1-> _V ) )
6	5	rexbidv	\|- ( a = f -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : f -1-1-> _V ) )
7	4 6	imbi12d	\|- ( a = f -> ( ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) )
8	2 7	raleqbidv	\|- ( a = f -> ( A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) )
9	8	imbi2d	\|- ( a = f -> ( ( b e. Fin -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) <-> ( b e. Fin -> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) ) )
10		xpeq1	\|- ( a = A -> ( a X. b ) = ( A X. b ) )
11	10	pweqd	\|- ( a = A -> ~P ( a X. b ) = ~P ( A X. b ) )
12		pweq	\|- ( a = A -> ~P a = ~P A )
13	12	raleqdv	\|- ( a = A -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P A d ~<_ ( c " d ) ) )
14		f1eq2	\|- ( a = A -> ( e : a -1-1-> _V <-> e : A -1-1-> _V ) )
15	14	rexbidv	\|- ( a = A -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : A -1-1-> _V ) )
16	13 15	imbi12d	\|- ( a = A -> ( ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> ( A. d e. ~P A d ~<_ ( c " d ) -> E. e e. ~P c e : A -1-1-> _V ) ) )
17	11 16	raleqbidv	\|- ( a = A -> ( A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. e e. ~P c e : A -1-1-> _V ) ) )
18	17	imbi2d	\|- ( a = A -> ( ( b e. Fin -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) <-> ( b e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. e e. ~P c e : A -1-1-> _V ) ) ) )
19		bi2.04	\|- ( ( a C. f -> ( b e. Fin -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) <-> ( b e. Fin -> ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) )
20	19	albii	\|- ( A. a ( a C. f -> ( b e. Fin -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) <-> A. a ( b e. Fin -> ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) )
21		19.21v	\|- ( A. a ( b e. Fin -> ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) <-> ( b e. Fin -> A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) )
22	20 21	bitri	\|- ( A. a ( a C. f -> ( b e. Fin -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) <-> ( b e. Fin -> A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) )
23		0elpw	\|- (/) e. ~P g
24		f10	\|- (/) : (/) -1-1-> _V
25		f1eq1	\|- ( e = (/) -> ( e : (/) -1-1-> _V <-> (/) : (/) -1-1-> _V ) )
26	25	rspcev	\|- ( ( (/) e. ~P g /\ (/) : (/) -1-1-> _V ) -> E. e e. ~P g e : (/) -1-1-> _V )
27	23 24 26	mp2an	\|- E. e e. ~P g e : (/) -1-1-> _V
28		f1eq2	\|- ( f = (/) -> ( e : f -1-1-> _V <-> e : (/) -1-1-> _V ) )
29	28	rexbidv	\|- ( f = (/) -> ( E. e e. ~P g e : f -1-1-> _V <-> E. e e. ~P g e : (/) -1-1-> _V ) )
30	27 29	mpbiri	\|- ( f = (/) -> E. e e. ~P g e : f -1-1-> _V )
31	30	a1i	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( f = (/) -> E. e e. ~P g e : f -1-1-> _V ) )
32		n0	\|- ( f =/= (/) <-> E. i i e. f )
33		snelpwi	\|- ( i e. f -> { i } e. ~P f )
34		id	\|- ( d = { i } -> d = { i } )
35		imaeq2	\|- ( d = { i } -> ( g " d ) = ( g " { i } ) )
36	34 35	breq12d	\|- ( d = { i } -> ( d ~<_ ( g " d ) <-> { i } ~<_ ( g " { i } ) ) )
37	36	rspcva	\|- ( ( { i } e. ~P f /\ A. d e. ~P f d ~<_ ( g " d ) ) -> { i } ~<_ ( g " { i } ) )
38		vex	\|- i e. _V
39	38	snnz	\|- { i } =/= (/)
40		vsnex	\|- { i } e. _V
41	40	0sdom	\|- ( (/) ~< { i } <-> { i } =/= (/) )
42	39 41	mpbir	\|- (/) ~< { i }
43		sdomdomtr	\|- ( ( (/) ~< { i } /\ { i } ~<_ ( g " { i } ) ) -> (/) ~< ( g " { i } ) )
44	42 43	mpan	\|- ( { i } ~<_ ( g " { i } ) -> (/) ~< ( g " { i } ) )
45		vex	\|- g e. _V
46	45	imaex	\|- ( g " { i } ) e. _V
47	46	0sdom	\|- ( (/) ~< ( g " { i } ) <-> ( g " { i } ) =/= (/) )
48	44 47	sylib	\|- ( { i } ~<_ ( g " { i } ) -> ( g " { i } ) =/= (/) )
49	37 48	syl	\|- ( ( { i } e. ~P f /\ A. d e. ~P f d ~<_ ( g " d ) ) -> ( g " { i } ) =/= (/) )
50	49	expcom	\|- ( A. d e. ~P f d ~<_ ( g " d ) -> ( { i } e. ~P f -> ( g " { i } ) =/= (/) ) )
51	33 50	syl5	\|- ( A. d e. ~P f d ~<_ ( g " d ) -> ( i e. f -> ( g " { i } ) =/= (/) ) )
52	51	adantl	\|- ( ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) -> ( i e. f -> ( g " { i } ) =/= (/) ) )
53	52	ad2antlr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( i e. f -> ( g " { i } ) =/= (/) ) )
54	53	impr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) ) -> ( g " { i } ) =/= (/) )
55		n0	\|- ( ( g " { i } ) =/= (/) <-> E. j j e. ( g " { i } ) )
56	54 55	sylib	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) ) -> E. j j e. ( g " { i } ) )
57	45	imaex	\|- ( g " c ) e. _V
58	57	difexi	\|- ( ( g " c ) \ { j } ) e. _V
59	58	0dom	\|- (/) ~<_ ( ( g " c ) \ { j } )
60		breq1	\|- ( c = (/) -> ( c ~<_ ( ( g " c ) \ { j } ) <-> (/) ~<_ ( ( g " c ) \ { j } ) ) )
61	59 60	mpbiri	\|- ( c = (/) -> c ~<_ ( ( g " c ) \ { j } ) )
62	61	a1i	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ c e. ~P ( f \ { i } ) ) -> ( c = (/) -> c ~<_ ( ( g " c ) \ { j } ) ) )
63		simpll	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) )
64		elpwi	\|- ( c e. ~P ( f \ { i } ) -> c C_ ( f \ { i } ) )
65	64	ad2antrl	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c C_ ( f \ { i } ) )
66		difsnpss	\|- ( i e. f <-> ( f \ { i } ) C. f )
67	66	biimpi	\|- ( i e. f -> ( f \ { i } ) C. f )
68	67	ad2antlr	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> ( f \ { i } ) C. f )
69	65 68	sspsstrd	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c C. f )
70		simprr	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c =/= (/) )
71	69 70	jca	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> ( c C. f /\ c =/= (/) ) )
72		psseq1	\|- ( h = c -> ( h C. f <-> c C. f ) )
73		neeq1	\|- ( h = c -> ( h =/= (/) <-> c =/= (/) ) )
74	72 73	anbi12d	\|- ( h = c -> ( ( h C. f /\ h =/= (/) ) <-> ( c C. f /\ c =/= (/) ) ) )
75		id	\|- ( h = c -> h = c )
76		imaeq2	\|- ( h = c -> ( g " h ) = ( g " c ) )
77	75 76	breq12d	\|- ( h = c -> ( h ~< ( g " h ) <-> c ~< ( g " c ) ) )
78	74 77	imbi12d	\|- ( h = c -> ( ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) <-> ( ( c C. f /\ c =/= (/) ) -> c ~< ( g " c ) ) ) )
79	78	spvv	\|- ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) -> ( ( c C. f /\ c =/= (/) ) -> c ~< ( g " c ) ) )
80	63 71 79	sylc	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c ~< ( g " c ) )
81		domdifsn	\|- ( c ~< ( g " c ) -> c ~<_ ( ( g " c ) \ { j } ) )
82	80 81	syl	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ ( c e. ~P ( f \ { i } ) /\ c =/= (/) ) ) -> c ~<_ ( ( g " c ) \ { j } ) )
83	82	expr	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ c e. ~P ( f \ { i } ) ) -> ( c =/= (/) -> c ~<_ ( ( g " c ) \ { j } ) ) )
84	62 83	pm2.61dne	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) /\ c e. ~P ( f \ { i } ) ) -> c ~<_ ( ( g " c ) \ { j } ) )
85	84	adantlrr	\|- ( ( ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ c e. ~P ( f \ { i } ) ) -> c ~<_ ( ( g " c ) \ { j } ) )
86	85	adantll	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) /\ c e. ~P ( f \ { i } ) ) -> c ~<_ ( ( g " c ) \ { j } ) )
87		dfss2	\|- ( c C_ ( f \ { i } ) <-> ( c i^i ( f \ { i } ) ) = c )
88	64 87	sylib	\|- ( c e. ~P ( f \ { i } ) -> ( c i^i ( f \ { i } ) ) = c )
89	88	imaeq2d	\|- ( c e. ~P ( f \ { i } ) -> ( g " ( c i^i ( f \ { i } ) ) ) = ( g " c ) )
90	89	ineq1d	\|- ( c e. ~P ( f \ { i } ) -> ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) = ( ( g " c ) i^i ( b \ { j } ) ) )
91	90	adantl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) /\ c e. ~P ( f \ { i } ) ) -> ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) = ( ( g " c ) i^i ( b \ { j } ) ) )
92		indif2	\|- ( ( g " c ) i^i ( b \ { j } ) ) = ( ( ( g " c ) i^i b ) \ { j } )
93		imassrn	\|- ( g " c ) C_ ran g
94		elpwi	\|- ( g e. ~P ( f X. b ) -> g C_ ( f X. b ) )
95		rnss	\|- ( g C_ ( f X. b ) -> ran g C_ ran ( f X. b ) )
96		rnxpss	\|- ran ( f X. b ) C_ b
97	95 96	sstrdi	\|- ( g C_ ( f X. b ) -> ran g C_ b )
98	94 97	syl	\|- ( g e. ~P ( f X. b ) -> ran g C_ b )
99	93 98	sstrid	\|- ( g e. ~P ( f X. b ) -> ( g " c ) C_ b )
100		dfss2	\|- ( ( g " c ) C_ b <-> ( ( g " c ) i^i b ) = ( g " c ) )
101	99 100	sylib	\|- ( g e. ~P ( f X. b ) -> ( ( g " c ) i^i b ) = ( g " c ) )
102	101	difeq1d	\|- ( g e. ~P ( f X. b ) -> ( ( ( g " c ) i^i b ) \ { j } ) = ( ( g " c ) \ { j } ) )
103	102	ad2antrl	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> ( ( ( g " c ) i^i b ) \ { j } ) = ( ( g " c ) \ { j } ) )
104	92 103	eqtrid	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> ( ( g " c ) i^i ( b \ { j } ) ) = ( ( g " c ) \ { j } ) )
105	104	ad2antrr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) /\ c e. ~P ( f \ { i } ) ) -> ( ( g " c ) i^i ( b \ { j } ) ) = ( ( g " c ) \ { j } ) )
106	91 105	eqtrd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) /\ c e. ~P ( f \ { i } ) ) -> ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) = ( ( g " c ) \ { j } ) )
107	86 106	breqtrrd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) /\ c e. ~P ( f \ { i } ) ) -> c ~<_ ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) )
108	107	ralrimiva	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> A. c e. ~P ( f \ { i } ) c ~<_ ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) )
109		id	\|- ( c = d -> c = d )
110		imainrect	\|- ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " c ) = ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) )
111		imaeq2	\|- ( c = d -> ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " c ) = ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
112	110 111	eqtr3id	\|- ( c = d -> ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) = ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
113	109 112	breq12d	\|- ( c = d -> ( c ~<_ ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) <-> d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) ) )
114	113	cbvralvw	\|- ( A. c e. ~P ( f \ { i } ) c ~<_ ( ( g " ( c i^i ( f \ { i } ) ) ) i^i ( b \ { j } ) ) <-> A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
115	108 114	sylib	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
116	115	adantllr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
117		inss2	\|- ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ ( ( f \ { i } ) X. ( b \ { j } ) )
118		difss	\|- ( b \ { j } ) C_ b
119		xpss2	\|- ( ( b \ { j } ) C_ b -> ( ( f \ { i } ) X. ( b \ { j } ) ) C_ ( ( f \ { i } ) X. b ) )
120	118 119	ax-mp	\|- ( ( f \ { i } ) X. ( b \ { j } ) ) C_ ( ( f \ { i } ) X. b )
121	117 120	sstri	\|- ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ ( ( f \ { i } ) X. b )
122	45	inex1	\|- ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e. _V
123	122	elpw	\|- ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e. ~P ( ( f \ { i } ) X. b ) <-> ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ ( ( f \ { i } ) X. b ) )
124	121 123	mpbir	\|- ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e. ~P ( ( f \ { i } ) X. b )
125		simpllr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) )
126	67	adantr	\|- ( ( i e. f /\ j e. ( g " { i } ) ) -> ( f \ { i } ) C. f )
127	126	ad2antll	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> ( f \ { i } ) C. f )
128		vex	\|- f e. _V
129	128	difexi	\|- ( f \ { i } ) e. _V
130		psseq1	\|- ( a = ( f \ { i } ) -> ( a C. f <-> ( f \ { i } ) C. f ) )
131		xpeq1	\|- ( a = ( f \ { i } ) -> ( a X. b ) = ( ( f \ { i } ) X. b ) )
132	131	pweqd	\|- ( a = ( f \ { i } ) -> ~P ( a X. b ) = ~P ( ( f \ { i } ) X. b ) )
133		pweq	\|- ( a = ( f \ { i } ) -> ~P a = ~P ( f \ { i } ) )
134	133	raleqdv	\|- ( a = ( f \ { i } ) -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) ) )
135		f1eq2	\|- ( a = ( f \ { i } ) -> ( e : a -1-1-> _V <-> e : ( f \ { i } ) -1-1-> _V ) )
136	135	rexbidv	\|- ( a = ( f \ { i } ) -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) )
137	134 136	imbi12d	\|- ( a = ( f \ { i } ) -> ( ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) ) )
138	132 137	raleqbidv	\|- ( a = ( f \ { i } ) -> ( A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> A. c e. ~P ( ( f \ { i } ) X. b ) ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) ) )
139	130 138	imbi12d	\|- ( a = ( f \ { i } ) -> ( ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) <-> ( ( f \ { i } ) C. f -> A. c e. ~P ( ( f \ { i } ) X. b ) ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) ) ) )
140	129 139	spcv	\|- ( A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) -> ( ( f \ { i } ) C. f -> A. c e. ~P ( ( f \ { i } ) X. b ) ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) ) )
141	125 127 140	sylc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> A. c e. ~P ( ( f \ { i } ) X. b ) ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) )
142		imaeq1	\|- ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( c " d ) = ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) )
143	142	breq2d	\|- ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( d ~<_ ( c " d ) <-> d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) ) )
144	143	ralbidv	\|- ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) <-> A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) ) )
145		pweq	\|- ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ~P c = ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) )
146	145	rexeqdv	\|- ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( E. e e. ~P c e : ( f \ { i } ) -1-1-> _V <-> E. e e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e : ( f \ { i } ) -1-1-> _V ) )
147	144 146	imbi12d	\|- ( c = ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) <-> ( A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e : ( f \ { i } ) -1-1-> _V ) ) )
148	147	rspcva	\|- ( ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e. ~P ( ( f \ { i } ) X. b ) /\ A. c e. ~P ( ( f \ { i } ) X. b ) ( A. d e. ~P ( f \ { i } ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ { i } ) -1-1-> _V ) ) -> ( A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e : ( f \ { i } ) -1-1-> _V ) )
149	124 141 148	sylancr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> ( A. d e. ~P ( f \ { i } ) d ~<_ ( ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e : ( f \ { i } ) -1-1-> _V ) )
150	116 149	mpd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> E. e e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e : ( f \ { i } ) -1-1-> _V )
151		f1eq1	\|- ( e = k -> ( e : ( f \ { i } ) -1-1-> _V <-> k : ( f \ { i } ) -1-1-> _V ) )
152	151	cbvrexvw	\|- ( E. e e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) e : ( f \ { i } ) -1-1-> _V <-> E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V )
153	150 152	sylib	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V )
154		vex	\|- j e. _V
155	38 154	elimasn	\|- ( j e. ( g " { i } ) <-> <. i , j >. e. g )
156	155	biimpi	\|- ( j e. ( g " { i } ) -> <. i , j >. e. g )
157	156	snssd	\|- ( j e. ( g " { i } ) -> { <. i , j >. } C_ g )
158	157	ad2antlr	\|- ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> { <. i , j >. } C_ g )
159		elpwi	\|- ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> k C_ ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) )
160		inss1	\|- ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) C_ g
161	159 160	sstrdi	\|- ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> k C_ g )
162	161	adantl	\|- ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> k C_ g )
163	158 162	unssd	\|- ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> ( { <. i , j >. } u. k ) C_ g )
164	45	elpw2	\|- ( ( { <. i , j >. } u. k ) e. ~P g <-> ( { <. i , j >. } u. k ) C_ g )
165	163 164	sylibr	\|- ( ( ( i e. f /\ j e. ( g " { i } ) ) /\ k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) ) -> ( { <. i , j >. } u. k ) e. ~P g )
166	165	ad2ant2lr	\|- ( ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) ) -> ( { <. i , j >. } u. k ) e. ~P g )
167	38 154	f1osn	\|- { <. i , j >. } : { i } -1-1-onto-> { j }
168	167	a1i	\|- ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> { <. i , j >. } : { i } -1-1-onto-> { j } )
169		f1f1orn	\|- ( k : ( f \ { i } ) -1-1-> _V -> k : ( f \ { i } ) -1-1-onto-> ran k )
170	169	adantl	\|- ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> k : ( f \ { i } ) -1-1-onto-> ran k )
171		disjdif	\|- ( { i } i^i ( f \ { i } ) ) = (/)
172	171	a1i	\|- ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> ( { i } i^i ( f \ { i } ) ) = (/) )
173		incom	\|- ( { j } i^i ran k ) = ( ran k i^i { j } )
174	159 117	sstrdi	\|- ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> k C_ ( ( f \ { i } ) X. ( b \ { j } ) ) )
175		rnss	\|- ( k C_ ( ( f \ { i } ) X. ( b \ { j } ) ) -> ran k C_ ran ( ( f \ { i } ) X. ( b \ { j } ) ) )
176		rnxpss	\|- ran ( ( f \ { i } ) X. ( b \ { j } ) ) C_ ( b \ { j } )
177	175 176	sstrdi	\|- ( k C_ ( ( f \ { i } ) X. ( b \ { j } ) ) -> ran k C_ ( b \ { j } ) )
178	174 177	syl	\|- ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ran k C_ ( b \ { j } ) )
179		disjdifr	\|- ( ( b \ { j } ) i^i { j } ) = (/)
180		ssdisj	\|- ( ( ran k C_ ( b \ { j } ) /\ ( ( b \ { j } ) i^i { j } ) = (/) ) -> ( ran k i^i { j } ) = (/) )
181	178 179 180	sylancl	\|- ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( ran k i^i { j } ) = (/) )
182	173 181	eqtrid	\|- ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) -> ( { j } i^i ran k ) = (/) )
183	182	adantr	\|- ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> ( { j } i^i ran k ) = (/) )
184		f1oun	\|- ( ( ( { <. i , j >. } : { i } -1-1-onto-> { j } /\ k : ( f \ { i } ) -1-1-onto-> ran k ) /\ ( ( { i } i^i ( f \ { i } ) ) = (/) /\ ( { j } i^i ran k ) = (/) ) ) -> ( { <. i , j >. } u. k ) : ( { i } u. ( f \ { i } ) ) -1-1-onto-> ( { j } u. ran k ) )
185	168 170 172 183 184	syl22anc	\|- ( ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) -> ( { <. i , j >. } u. k ) : ( { i } u. ( f \ { i } ) ) -1-1-onto-> ( { j } u. ran k ) )
186	185	adantl	\|- ( ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) ) -> ( { <. i , j >. } u. k ) : ( { i } u. ( f \ { i } ) ) -1-1-onto-> ( { j } u. ran k ) )
187		snssi	\|- ( i e. f -> { i } C_ f )
188	187	ad2antrl	\|- ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) -> { i } C_ f )
189		undif	\|- ( { i } C_ f <-> ( { i } u. ( f \ { i } ) ) = f )
190	188 189	sylib	\|- ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) -> ( { i } u. ( f \ { i } ) ) = f )
191	190	f1oeq2d	\|- ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) -> ( ( { <. i , j >. } u. k ) : ( { i } u. ( f \ { i } ) ) -1-1-onto-> ( { j } u. ran k ) <-> ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) ) )
192	191	adantr	\|- ( ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) ) -> ( ( { <. i , j >. } u. k ) : ( { i } u. ( f \ { i } ) ) -1-1-onto-> ( { j } u. ran k ) <-> ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) ) )
193	186 192	mpbid	\|- ( ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) ) -> ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) )
194		f1of1	\|- ( ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) -> ( { <. i , j >. } u. k ) : f -1-1-> ( { j } u. ran k ) )
195		ssv	\|- ( { j } u. ran k ) C_ _V
196		f1ss	\|- ( ( ( { <. i , j >. } u. k ) : f -1-1-> ( { j } u. ran k ) /\ ( { j } u. ran k ) C_ _V ) -> ( { <. i , j >. } u. k ) : f -1-1-> _V )
197	194 195 196	sylancl	\|- ( ( { <. i , j >. } u. k ) : f -1-1-onto-> ( { j } u. ran k ) -> ( { <. i , j >. } u. k ) : f -1-1-> _V )
198	193 197	syl	\|- ( ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) ) -> ( { <. i , j >. } u. k ) : f -1-1-> _V )
199		f1eq1	\|- ( e = ( { <. i , j >. } u. k ) -> ( e : f -1-1-> _V <-> ( { <. i , j >. } u. k ) : f -1-1-> _V ) )
200	199	rspcev	\|- ( ( ( { <. i , j >. } u. k ) e. ~P g /\ ( { <. i , j >. } u. k ) : f -1-1-> _V ) -> E. e e. ~P g e : f -1-1-> _V )
201	166 198 200	syl2anc	\|- ( ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) /\ ( k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) /\ k : ( f \ { i } ) -1-1-> _V ) ) -> E. e e. ~P g e : f -1-1-> _V )
202	201	rexlimdvaa	\|- ( ( g e. ~P ( f X. b ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) -> ( E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) )
203	202	ex	\|- ( g e. ~P ( f X. b ) -> ( ( i e. f /\ j e. ( g " { i } ) ) -> ( E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
204	203	adantr	\|- ( ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) -> ( ( i e. f /\ j e. ( g " { i } ) ) -> ( E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
205	204	ad2antlr	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( ( i e. f /\ j e. ( g " { i } ) ) -> ( E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
206	205	impr	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> ( E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) )
207	206	adantllr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> ( E. k e. ~P ( g i^i ( ( f \ { i } ) X. ( b \ { j } ) ) ) k : ( f \ { i } ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) )
208	153 207	mpd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ ( i e. f /\ j e. ( g " { i } ) ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
209	208	expr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( ( i e. f /\ j e. ( g " { i } ) ) -> E. e e. ~P g e : f -1-1-> _V ) )
210	209	expd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( i e. f -> ( j e. ( g " { i } ) -> E. e e. ~P g e : f -1-1-> _V ) ) )
211	210	impr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) ) -> ( j e. ( g " { i } ) -> E. e e. ~P g e : f -1-1-> _V ) )
212	211	exlimdv	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) ) -> ( E. j j e. ( g " { i } ) -> E. e e. ~P g e : f -1-1-> _V ) )
213	56 212	mpd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) /\ i e. f ) ) -> E. e e. ~P g e : f -1-1-> _V )
214	213	expr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( i e. f -> E. e e. ~P g e : f -1-1-> _V ) )
215	214	exlimdv	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( E. i i e. f -> E. e e. ~P g e : f -1-1-> _V ) )
216	32 215	biimtrid	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> ( f =/= (/) -> E. e e. ~P g e : f -1-1-> _V ) )
217	31 216	pm2.61dne	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
218		exanali	\|- ( E. h ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) <-> -. A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) )
219		simprll	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> h C. f )
220		pssss	\|- ( h C. f -> h C_ f )
221	219 220	syl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> h C_ f )
222	221	sspwd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> ~P h C_ ~P f )
223		simplrr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. d e. ~P f d ~<_ ( g " d ) )
224		ssralv	\|- ( ~P h C_ ~P f -> ( A. d e. ~P f d ~<_ ( g " d ) -> A. d e. ~P h d ~<_ ( g " d ) ) )
225	222 223 224	sylc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. d e. ~P h d ~<_ ( g " d ) )
226		elpwi	\|- ( d e. ~P h -> d C_ h )
227		resima2	\|- ( d C_ h -> ( ( g \|` h ) " d ) = ( g " d ) )
228	226 227	syl	\|- ( d e. ~P h -> ( ( g \|` h ) " d ) = ( g " d ) )
229	228	eqcomd	\|- ( d e. ~P h -> ( g " d ) = ( ( g \|` h ) " d ) )
230	229	breq2d	\|- ( d e. ~P h -> ( d ~<_ ( g " d ) <-> d ~<_ ( ( g \|` h ) " d ) ) )
231	230	ralbiia	\|- ( A. d e. ~P h d ~<_ ( g " d ) <-> A. d e. ~P h d ~<_ ( ( g \|` h ) " d ) )
232	225 231	sylib	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. d e. ~P h d ~<_ ( ( g \|` h ) " d ) )
233		imaeq1	\|- ( c = ( g \|` h ) -> ( c " d ) = ( ( g \|` h ) " d ) )
234	233	breq2d	\|- ( c = ( g \|` h ) -> ( d ~<_ ( c " d ) <-> d ~<_ ( ( g \|` h ) " d ) ) )
235	234	ralbidv	\|- ( c = ( g \|` h ) -> ( A. d e. ~P h d ~<_ ( c " d ) <-> A. d e. ~P h d ~<_ ( ( g \|` h ) " d ) ) )
236		pweq	\|- ( c = ( g \|` h ) -> ~P c = ~P ( g \|` h ) )
237	236	rexeqdv	\|- ( c = ( g \|` h ) -> ( E. e e. ~P c e : h -1-1-> _V <-> E. e e. ~P ( g \|` h ) e : h -1-1-> _V ) )
238	235 237	imbi12d	\|- ( c = ( g \|` h ) -> ( ( A. d e. ~P h d ~<_ ( c " d ) -> E. e e. ~P c e : h -1-1-> _V ) <-> ( A. d e. ~P h d ~<_ ( ( g \|` h ) " d ) -> E. e e. ~P ( g \|` h ) e : h -1-1-> _V ) ) )
239		simpllr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) )
240		psseq1	\|- ( a = h -> ( a C. f <-> h C. f ) )
241		xpeq1	\|- ( a = h -> ( a X. b ) = ( h X. b ) )
242	241	pweqd	\|- ( a = h -> ~P ( a X. b ) = ~P ( h X. b ) )
243		pweq	\|- ( a = h -> ~P a = ~P h )
244	243	raleqdv	\|- ( a = h -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P h d ~<_ ( c " d ) ) )
245		f1eq2	\|- ( a = h -> ( e : a -1-1-> _V <-> e : h -1-1-> _V ) )
246	245	rexbidv	\|- ( a = h -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : h -1-1-> _V ) )
247	244 246	imbi12d	\|- ( a = h -> ( ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> ( A. d e. ~P h d ~<_ ( c " d ) -> E. e e. ~P c e : h -1-1-> _V ) ) )
248	242 247	raleqbidv	\|- ( a = h -> ( A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> A. c e. ~P ( h X. b ) ( A. d e. ~P h d ~<_ ( c " d ) -> E. e e. ~P c e : h -1-1-> _V ) ) )
249	240 248	imbi12d	\|- ( a = h -> ( ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) <-> ( h C. f -> A. c e. ~P ( h X. b ) ( A. d e. ~P h d ~<_ ( c " d ) -> E. e e. ~P c e : h -1-1-> _V ) ) ) )
250	249	spvv	\|- ( A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) -> ( h C. f -> A. c e. ~P ( h X. b ) ( A. d e. ~P h d ~<_ ( c " d ) -> E. e e. ~P c e : h -1-1-> _V ) ) )
251	239 219 250	sylc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. c e. ~P ( h X. b ) ( A. d e. ~P h d ~<_ ( c " d ) -> E. e e. ~P c e : h -1-1-> _V ) )
252		simplrl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> g e. ~P ( f X. b ) )
253		ssres	\|- ( g C_ ( f X. b ) -> ( g \|` h ) C_ ( ( f X. b ) \|` h ) )
254		df-res	\|- ( ( f X. b ) \|` h ) = ( ( f X. b ) i^i ( h X. _V ) )
255		inxp	\|- ( ( f X. b ) i^i ( h X. _V ) ) = ( ( f i^i h ) X. ( b i^i _V ) )
256		inss2	\|- ( f i^i h ) C_ h
257		inss1	\|- ( b i^i _V ) C_ b
258		xpss12	\|- ( ( ( f i^i h ) C_ h /\ ( b i^i _V ) C_ b ) -> ( ( f i^i h ) X. ( b i^i _V ) ) C_ ( h X. b ) )
259	256 257 258	mp2an	\|- ( ( f i^i h ) X. ( b i^i _V ) ) C_ ( h X. b )
260	255 259	eqsstri	\|- ( ( f X. b ) i^i ( h X. _V ) ) C_ ( h X. b )
261	254 260	eqsstri	\|- ( ( f X. b ) \|` h ) C_ ( h X. b )
262	253 261	sstrdi	\|- ( g C_ ( f X. b ) -> ( g \|` h ) C_ ( h X. b ) )
263	94 262	syl	\|- ( g e. ~P ( f X. b ) -> ( g \|` h ) C_ ( h X. b ) )
264	45	resex	\|- ( g \|` h ) e. _V
265	264	elpw	\|- ( ( g \|` h ) e. ~P ( h X. b ) <-> ( g \|` h ) C_ ( h X. b ) )
266	263 265	sylibr	\|- ( g e. ~P ( f X. b ) -> ( g \|` h ) e. ~P ( h X. b ) )
267	252 266	syl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> ( g \|` h ) e. ~P ( h X. b ) )
268	238 251 267	rspcdva	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> ( A. d e. ~P h d ~<_ ( ( g \|` h ) " d ) -> E. e e. ~P ( g \|` h ) e : h -1-1-> _V ) )
269	232 268	mpd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. e e. ~P ( g \|` h ) e : h -1-1-> _V )
270		f1eq1	\|- ( e = i -> ( e : h -1-1-> _V <-> i : h -1-1-> _V ) )
271	270	cbvrexvw	\|- ( E. e e. ~P ( g \|` h ) e : h -1-1-> _V <-> E. i e. ~P ( g \|` h ) i : h -1-1-> _V )
272	269 271	sylib	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. i e. ~P ( g \|` h ) i : h -1-1-> _V )
273		id	\|- ( d = ( h u. c ) -> d = ( h u. c ) )
274		imaeq2	\|- ( d = ( h u. c ) -> ( g " d ) = ( g " ( h u. c ) ) )
275	273 274	breq12d	\|- ( d = ( h u. c ) -> ( d ~<_ ( g " d ) <-> ( h u. c ) ~<_ ( g " ( h u. c ) ) ) )
276		simprr	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> A. d e. ~P f d ~<_ ( g " d ) )
277	276	ad2antrr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> A. d e. ~P f d ~<_ ( g " d ) )
278	220	ad2antrr	\|- ( ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) -> h C_ f )
279	278	ad2antlr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> h C_ f )
280		elpwi	\|- ( c e. ~P ( f \ h ) -> c C_ ( f \ h ) )
281		difss	\|- ( f \ h ) C_ f
282	280 281	sstrdi	\|- ( c e. ~P ( f \ h ) -> c C_ f )
283	282	adantl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> c C_ f )
284	279 283	unssd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( h u. c ) C_ f )
285	128	elpw2	\|- ( ( h u. c ) e. ~P f <-> ( h u. c ) C_ f )
286	284 285	sylibr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( h u. c ) e. ~P f )
287	275 277 286	rspcdva	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( h u. c ) ~<_ ( g " ( h u. c ) ) )
288		imaundi	\|- ( g " ( h u. c ) ) = ( ( g " h ) u. ( g " c ) )
289		undif2	\|- ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) ) = ( ( g " h ) u. ( g " c ) )
290	288 289	eqtr4i	\|- ( g " ( h u. c ) ) = ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) )
291	287 290	breqtrdi	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( h u. c ) ~<_ ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) ) )
292		simp-4l	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> f e. Fin )
293	292 279	ssfid	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> h e. Fin )
294		id	\|- ( d = h -> d = h )
295		imaeq2	\|- ( d = h -> ( g " d ) = ( g " h ) )
296	294 295	breq12d	\|- ( d = h -> ( d ~<_ ( g " d ) <-> h ~<_ ( g " h ) ) )
297		vex	\|- h e. _V
298	297	elpw	\|- ( h e. ~P f <-> h C_ f )
299	279 298	sylibr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> h e. ~P f )
300	296 277 299	rspcdva	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> h ~<_ ( g " h ) )
301		simplrr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> -. h ~< ( g " h ) )
302		bren2	\|- ( h ~~ ( g " h ) <-> ( h ~<_ ( g " h ) /\ -. h ~< ( g " h ) ) )
303	300 301 302	sylanbrc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> h ~~ ( g " h ) )
304	303	ensymd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( g " h ) ~~ h )
305		incom	\|- ( h i^i c ) = ( c i^i h )
306		ssdifin0	\|- ( c C_ ( f \ h ) -> ( c i^i h ) = (/) )
307	305 306	eqtrid	\|- ( c C_ ( f \ h ) -> ( h i^i c ) = (/) )
308	280 307	syl	\|- ( c e. ~P ( f \ h ) -> ( h i^i c ) = (/) )
309	308	adantl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( h i^i c ) = (/) )
310		disjdif	\|- ( ( g " h ) i^i ( ( g " c ) \ ( g " h ) ) ) = (/)
311	310	a1i	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( ( g " h ) i^i ( ( g " c ) \ ( g " h ) ) ) = (/) )
312		domunfican	\|- ( ( ( h e. Fin /\ ( g " h ) ~~ h ) /\ ( ( h i^i c ) = (/) /\ ( ( g " h ) i^i ( ( g " c ) \ ( g " h ) ) ) = (/) ) ) -> ( ( h u. c ) ~<_ ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) ) <-> c ~<_ ( ( g " c ) \ ( g " h ) ) ) )
313	293 304 309 311 312	syl22anc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( ( h u. c ) ~<_ ( ( g " h ) u. ( ( g " c ) \ ( g " h ) ) ) <-> c ~<_ ( ( g " c ) \ ( g " h ) ) ) )
314	291 313	mpbid	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> c ~<_ ( ( g " c ) \ ( g " h ) ) )
315	101	difeq1d	\|- ( g e. ~P ( f X. b ) -> ( ( ( g " c ) i^i b ) \ ( g " h ) ) = ( ( g " c ) \ ( g " h ) ) )
316	315	ad2antrl	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> ( ( ( g " c ) i^i b ) \ ( g " h ) ) = ( ( g " c ) \ ( g " h ) ) )
317	316	ad2antrr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( ( ( g " c ) i^i b ) \ ( g " h ) ) = ( ( g " c ) \ ( g " h ) ) )
318	314 317	breqtrrd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> c ~<_ ( ( ( g " c ) i^i b ) \ ( g " h ) ) )
319		dfss2	\|- ( c C_ ( f \ h ) <-> ( c i^i ( f \ h ) ) = c )
320	280 319	sylib	\|- ( c e. ~P ( f \ h ) -> ( c i^i ( f \ h ) ) = c )
321	320	imaeq2d	\|- ( c e. ~P ( f \ h ) -> ( g " ( c i^i ( f \ h ) ) ) = ( g " c ) )
322	321	ineq1d	\|- ( c e. ~P ( f \ h ) -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( g " c ) i^i ( b \ ( g " h ) ) ) )
323		indif2	\|- ( ( g " c ) i^i ( b \ ( g " h ) ) ) = ( ( ( g " c ) i^i b ) \ ( g " h ) )
324	322 323	eqtrdi	\|- ( c e. ~P ( f \ h ) -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( ( g " c ) i^i b ) \ ( g " h ) ) )
325	324	adantl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( ( g " c ) i^i b ) \ ( g " h ) ) )
326	318 325	breqtrrd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) /\ c e. ~P ( f \ h ) ) -> c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) )
327	326	ralrimiva	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. c e. ~P ( f \ h ) c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) )
328		imainrect	\|- ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " c ) = ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) )
329		imaeq2	\|- ( c = d -> ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " c ) = ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
330	328 329	eqtr3id	\|- ( c = d -> ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) = ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
331	109 330	breq12d	\|- ( c = d -> ( c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) <-> d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) ) )
332	331	cbvralvw	\|- ( A. c e. ~P ( f \ h ) c ~<_ ( ( g " ( c i^i ( f \ h ) ) ) i^i ( b \ ( g " h ) ) ) <-> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
333	327 332	sylib	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
334	333	adantllr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
335		inss2	\|- ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ ( ( f \ h ) X. ( b \ ( g " h ) ) )
336		difss	\|- ( b \ ( g " h ) ) C_ b
337		xpss2	\|- ( ( b \ ( g " h ) ) C_ b -> ( ( f \ h ) X. ( b \ ( g " h ) ) ) C_ ( ( f \ h ) X. b ) )
338	336 337	ax-mp	\|- ( ( f \ h ) X. ( b \ ( g " h ) ) ) C_ ( ( f \ h ) X. b )
339	335 338	sstri	\|- ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ ( ( f \ h ) X. b )
340	45	inex1	\|- ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. _V
341	340	elpw	\|- ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. ~P ( ( f \ h ) X. b ) <-> ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ ( ( f \ h ) X. b ) )
342	339 341	mpbir	\|- ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. ~P ( ( f \ h ) X. b )
343		incom	\|- ( f i^i h ) = ( h i^i f )
344		dfss2	\|- ( h C_ f <-> ( h i^i f ) = h )
345	220 344	sylib	\|- ( h C. f -> ( h i^i f ) = h )
346	343 345	eqtrid	\|- ( h C. f -> ( f i^i h ) = h )
347	346	neeq1d	\|- ( h C. f -> ( ( f i^i h ) =/= (/) <-> h =/= (/) ) )
348	347	biimpar	\|- ( ( h C. f /\ h =/= (/) ) -> ( f i^i h ) =/= (/) )
349		disj4	\|- ( ( f i^i h ) = (/) <-> -. ( f \ h ) C. f )
350	349	bicomi	\|- ( -. ( f \ h ) C. f <-> ( f i^i h ) = (/) )
351	350	necon1abii	\|- ( ( f i^i h ) =/= (/) <-> ( f \ h ) C. f )
352	348 351	sylib	\|- ( ( h C. f /\ h =/= (/) ) -> ( f \ h ) C. f )
353	352	ad2antrl	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> ( f \ h ) C. f )
354	128	difexi	\|- ( f \ h ) e. _V
355		psseq1	\|- ( a = ( f \ h ) -> ( a C. f <-> ( f \ h ) C. f ) )
356		xpeq1	\|- ( a = ( f \ h ) -> ( a X. b ) = ( ( f \ h ) X. b ) )
357	356	pweqd	\|- ( a = ( f \ h ) -> ~P ( a X. b ) = ~P ( ( f \ h ) X. b ) )
358		pweq	\|- ( a = ( f \ h ) -> ~P a = ~P ( f \ h ) )
359	358	raleqdv	\|- ( a = ( f \ h ) -> ( A. d e. ~P a d ~<_ ( c " d ) <-> A. d e. ~P ( f \ h ) d ~<_ ( c " d ) ) )
360		f1eq2	\|- ( a = ( f \ h ) -> ( e : a -1-1-> _V <-> e : ( f \ h ) -1-1-> _V ) )
361	360	rexbidv	\|- ( a = ( f \ h ) -> ( E. e e. ~P c e : a -1-1-> _V <-> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) )
362	359 361	imbi12d	\|- ( a = ( f \ h ) -> ( ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) )
363	357 362	raleqbidv	\|- ( a = ( f \ h ) -> ( A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) <-> A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) )
364	355 363	imbi12d	\|- ( a = ( f \ h ) -> ( ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) <-> ( ( f \ h ) C. f -> A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) ) )
365	354 364	spcv	\|- ( A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) -> ( ( f \ h ) C. f -> A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) )
366	239 353 365	sylc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) )
367		imaeq1	\|- ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( c " d ) = ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) )
368	367	breq2d	\|- ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( d ~<_ ( c " d ) <-> d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) ) )
369	368	ralbidv	\|- ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) <-> A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) ) )
370		pweq	\|- ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ~P c = ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) )
371	370	rexeqdv	\|- ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( E. e e. ~P c e : ( f \ h ) -1-1-> _V <-> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) )
372	369 371	imbi12d	\|- ( c = ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ( ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) <-> ( A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) ) )
373	372	rspcva	\|- ( ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e. ~P ( ( f \ h ) X. b ) /\ A. c e. ~P ( ( f \ h ) X. b ) ( A. d e. ~P ( f \ h ) d ~<_ ( c " d ) -> E. e e. ~P c e : ( f \ h ) -1-1-> _V ) ) -> ( A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) )
374	342 366 373	sylancr	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> ( A. d e. ~P ( f \ h ) d ~<_ ( ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) " d ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V ) )
375	334 374	mpd	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V )
376		f1eq1	\|- ( e = j -> ( e : ( f \ h ) -1-1-> _V <-> j : ( f \ h ) -1-1-> _V ) )
377	376	cbvrexvw	\|- ( E. e e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) e : ( f \ h ) -1-1-> _V <-> E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V )
378	375 377	sylib	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V )
379		elpwi	\|- ( i e. ~P ( g \|` h ) -> i C_ ( g \|` h ) )
380		resss	\|- ( g \|` h ) C_ g
381	379 380	sstrdi	\|- ( i e. ~P ( g \|` h ) -> i C_ g )
382	381	adantr	\|- ( ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) -> i C_ g )
383	382	ad2antlr	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> i C_ g )
384		elpwi	\|- ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> j C_ ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) )
385		inss1	\|- ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) C_ g
386	384 385	sstrdi	\|- ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> j C_ g )
387	386	ad2antrl	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> j C_ g )
388	383 387	unssd	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) C_ g )
389	45	elpw2	\|- ( ( i u. j ) e. ~P g <-> ( i u. j ) C_ g )
390	388 389	sylibr	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) e. ~P g )
391		f1f1orn	\|- ( i : h -1-1-> _V -> i : h -1-1-onto-> ran i )
392	391	adantl	\|- ( ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) -> i : h -1-1-onto-> ran i )
393	392	ad2antlr	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> i : h -1-1-onto-> ran i )
394		f1f1orn	\|- ( j : ( f \ h ) -1-1-> _V -> j : ( f \ h ) -1-1-onto-> ran j )
395	394	ad2antll	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> j : ( f \ h ) -1-1-onto-> ran j )
396		disjdif	\|- ( h i^i ( f \ h ) ) = (/)
397	396	a1i	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( h i^i ( f \ h ) ) = (/) )
398		rnss	\|- ( i C_ ( g \|` h ) -> ran i C_ ran ( g \|` h ) )
399	379 398	syl	\|- ( i e. ~P ( g \|` h ) -> ran i C_ ran ( g \|` h ) )
400		df-ima	\|- ( g " h ) = ran ( g \|` h )
401	399 400	sseqtrrdi	\|- ( i e. ~P ( g \|` h ) -> ran i C_ ( g " h ) )
402	401	adantr	\|- ( ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) -> ran i C_ ( g " h ) )
403	402	ad2antlr	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ran i C_ ( g " h ) )
404		incom	\|- ( ( g " h ) i^i ran j ) = ( ran j i^i ( g " h ) )
405	384 335	sstrdi	\|- ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> j C_ ( ( f \ h ) X. ( b \ ( g " h ) ) ) )
406		rnss	\|- ( j C_ ( ( f \ h ) X. ( b \ ( g " h ) ) ) -> ran j C_ ran ( ( f \ h ) X. ( b \ ( g " h ) ) ) )
407	405 406	syl	\|- ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ran j C_ ran ( ( f \ h ) X. ( b \ ( g " h ) ) ) )
408		rnxpss	\|- ran ( ( f \ h ) X. ( b \ ( g " h ) ) ) C_ ( b \ ( g " h ) )
409	407 408	sstrdi	\|- ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) -> ran j C_ ( b \ ( g " h ) ) )
410	409	ad2antrl	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ran j C_ ( b \ ( g " h ) ) )
411		disjdifr	\|- ( ( b \ ( g " h ) ) i^i ( g " h ) ) = (/)
412		ssdisj	\|- ( ( ran j C_ ( b \ ( g " h ) ) /\ ( ( b \ ( g " h ) ) i^i ( g " h ) ) = (/) ) -> ( ran j i^i ( g " h ) ) = (/) )
413	410 411 412	sylancl	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ran j i^i ( g " h ) ) = (/) )
414	404 413	eqtrid	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ( g " h ) i^i ran j ) = (/) )
415		ssdisj	\|- ( ( ran i C_ ( g " h ) /\ ( ( g " h ) i^i ran j ) = (/) ) -> ( ran i i^i ran j ) = (/) )
416	403 414 415	syl2anc	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ran i i^i ran j ) = (/) )
417		f1oun	\|- ( ( ( i : h -1-1-onto-> ran i /\ j : ( f \ h ) -1-1-onto-> ran j ) /\ ( ( h i^i ( f \ h ) ) = (/) /\ ( ran i i^i ran j ) = (/) ) ) -> ( i u. j ) : ( h u. ( f \ h ) ) -1-1-onto-> ( ran i u. ran j ) )
418	393 395 397 416 417	syl22anc	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : ( h u. ( f \ h ) ) -1-1-onto-> ( ran i u. ran j ) )
419		undif	\|- ( h C_ f <-> ( h u. ( f \ h ) ) = f )
420	419	biimpi	\|- ( h C_ f -> ( h u. ( f \ h ) ) = f )
421	420	adantl	\|- ( ( g e. ~P ( f X. b ) /\ h C_ f ) -> ( h u. ( f \ h ) ) = f )
422	421	ad2antrr	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( h u. ( f \ h ) ) = f )
423	422	f1oeq2d	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( ( i u. j ) : ( h u. ( f \ h ) ) -1-1-onto-> ( ran i u. ran j ) <-> ( i u. j ) : f -1-1-onto-> ( ran i u. ran j ) ) )
424	418 423	mpbid	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : f -1-1-onto-> ( ran i u. ran j ) )
425		f1of1	\|- ( ( i u. j ) : f -1-1-onto-> ( ran i u. ran j ) -> ( i u. j ) : f -1-1-> ( ran i u. ran j ) )
426	424 425	syl	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : f -1-1-> ( ran i u. ran j ) )
427		ssv	\|- ( ran i u. ran j ) C_ _V
428		f1ss	\|- ( ( ( i u. j ) : f -1-1-> ( ran i u. ran j ) /\ ( ran i u. ran j ) C_ _V ) -> ( i u. j ) : f -1-1-> _V )
429	426 427 428	sylancl	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> ( i u. j ) : f -1-1-> _V )
430		f1eq1	\|- ( e = ( i u. j ) -> ( e : f -1-1-> _V <-> ( i u. j ) : f -1-1-> _V ) )
431	430	rspcev	\|- ( ( ( i u. j ) e. ~P g /\ ( i u. j ) : f -1-1-> _V ) -> E. e e. ~P g e : f -1-1-> _V )
432	390 429 431	syl2anc	\|- ( ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) /\ ( j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) /\ j : ( f \ h ) -1-1-> _V ) ) -> E. e e. ~P g e : f -1-1-> _V )
433	432	rexlimdvaa	\|- ( ( ( g e. ~P ( f X. b ) /\ h C_ f ) /\ ( i e. ~P ( g \|` h ) /\ i : h -1-1-> _V ) ) -> ( E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) )
434	433	rexlimdvaa	\|- ( ( g e. ~P ( f X. b ) /\ h C_ f ) -> ( E. i e. ~P ( g \|` h ) i : h -1-1-> _V -> ( E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
435	252 221 434	syl2anc	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> ( E. i e. ~P ( g \|` h ) i : h -1-1-> _V -> ( E. j e. ~P ( g i^i ( ( f \ h ) X. ( b \ ( g " h ) ) ) ) j : ( f \ h ) -1-1-> _V -> E. e e. ~P g e : f -1-1-> _V ) ) )
436	272 378 435	mp2d	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
437	436	ex	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> ( ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) -> E. e e. ~P g e : f -1-1-> _V ) )
438	437	exlimdv	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> ( E. h ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) -> E. e e. ~P g e : f -1-1-> _V ) )
439	438	imp	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ E. h ( ( h C. f /\ h =/= (/) ) /\ -. h ~< ( g " h ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
440	218 439	sylan2br	\|- ( ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) /\ -. A. h ( ( h C. f /\ h =/= (/) ) -> h ~< ( g " h ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
441	217 440	pm2.61dan	\|- ( ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) /\ ( g e. ~P ( f X. b ) /\ A. d e. ~P f d ~<_ ( g " d ) ) ) -> E. e e. ~P g e : f -1-1-> _V )
442	441	exp32	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) -> ( g e. ~P ( f X. b ) -> ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -1-1-> _V ) ) )
443	442	ralrimiv	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) -> A. g e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -1-1-> _V ) )
444		imaeq1	\|- ( g = c -> ( g " d ) = ( c " d ) )
445	444	breq2d	\|- ( g = c -> ( d ~<_ ( g " d ) <-> d ~<_ ( c " d ) ) )
446	445	ralbidv	\|- ( g = c -> ( A. d e. ~P f d ~<_ ( g " d ) <-> A. d e. ~P f d ~<_ ( c " d ) ) )
447		pweq	\|- ( g = c -> ~P g = ~P c )
448	447	rexeqdv	\|- ( g = c -> ( E. e e. ~P g e : f -1-1-> _V <-> E. e e. ~P c e : f -1-1-> _V ) )
449	446 448	imbi12d	\|- ( g = c -> ( ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -1-1-> _V ) <-> ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) )
450	449	cbvralvw	\|- ( A. g e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( g " d ) -> E. e e. ~P g e : f -1-1-> _V ) <-> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) )
451	443 450	sylib	\|- ( ( ( f e. Fin /\ b e. Fin ) /\ A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) -> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) )
452	451	exp31	\|- ( f e. Fin -> ( b e. Fin -> ( A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) -> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) ) )
453	452	a2d	\|- ( f e. Fin -> ( ( b e. Fin -> A. a ( a C. f -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) -> ( b e. Fin -> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) ) )
454	22 453	biimtrid	\|- ( f e. Fin -> ( A. a ( a C. f -> ( b e. Fin -> A. c e. ~P ( a X. b ) ( A. d e. ~P a d ~<_ ( c " d ) -> E. e e. ~P c e : a -1-1-> _V ) ) ) -> ( b e. Fin -> A. c e. ~P ( f X. b ) ( A. d e. ~P f d ~<_ ( c " d ) -> E. e e. ~P c e : f -1-1-> _V ) ) ) )
455	9 18 454	findcard3	\|- ( A e. Fin -> ( b e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. e e. ~P c e : A -1-1-> _V ) ) )

Metamath Proof Explorer

Theorem marypha1lem

Proof