Theorem sfinltfin 4535

Description: Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
sfinltfin	|- ((( Sfin (M, N) /\ Sfin (P, Q)) /\ <<M, P>> e. <fin ) -> <<N, Q>> e. <fin )

Proof of Theorem sfinltfin

Dummy variables a b r s d g t x n u m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sfin 4446	. . 3 |- ( Sfin (M, N) <-> (M e. Nn /\ N e. Nn /\ E.a(~P1 a e. M /\ ~Pa e. N)))
2		df-sfin 4446	. . 3 |- ( Sfin (P, Q) <-> (P e. Nn /\ Q e. Nn /\ E.b(~P1 b e. P /\ ~Pb e. Q)))
3		3an6 1262	. . . 4 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ (E.a(~P1 a e. M /\ ~Pa e. N) /\ E.b(~P1 b e. P /\ ~Pb e. Q))) <-> ((M e. Nn /\ N e. Nn /\ E.a(~P1 a e. M /\ ~Pa e. N)) /\ (P e. Nn /\ Q e. Nn /\ E.b(~P1 b e. P /\ ~Pb e. Q))))
4		eeanv 1913	. . . . . 6 |- (E.aE.b((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q)) <-> (E.a(~P1 a e. M /\ ~Pa e. N) /\ E.b(~P1 b e. P /\ ~Pb e. Q)))
5		simp1l 979	. . . . . . . . . 10 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> M e. Nn )
6		simp3ll 1026	. . . . . . . . . 10 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ~P1 a e. M)
7		ncfinlower 4483	. . . . . . . . . 10 |- ((M e. Nn /\ ~P1 a e. M /\ ~P1 a e. M) -> E.r e. Nn (a e. r /\ a e. r))
8	5, 6, 6, 7	syl3anc 1182	. . . . . . . . 9 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> E.r e. Nn (a e. r /\ a e. r))
9		simp1r 980	. . . . . . . . . 10 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> P e. Nn )
10		simp3rl 1028	. . . . . . . . . 10 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ~P1 b e. P)
11		ncfinlower 4483	. . . . . . . . . 10 |- ((P e. Nn /\ ~P1 b e. P /\ ~P1 b e. P) -> E.s e. Nn (b e. s /\ b e. s))
12	9, 10, 10, 11	syl3anc 1182	. . . . . . . . 9 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> E.s e. Nn (b e. s /\ b e. s))
13		reeanv 2778	. . . . . . . . . 10 |- (E.r e. Nn E.s e. Nn ((a e. r /\ a e. r) /\ (b e. s /\ b e. s)) <-> (E.r e. Nn (a e. r /\ a e. r) /\ E.s e. Nn (b e. s /\ b e. s)))
14		simpl 443	. . . . . . . . . . . . 13 |- ((a e. r /\ a e. r) -> a e. r)
15		simpl 443	. . . . . . . . . . . . 13 |- ((b e. s /\ b e. s) -> b e. s)
16	14, 15	anim12i 549	. . . . . . . . . . . 12 |- (((a e. r /\ a e. r) /\ (b e. s /\ b e. s)) -> (a e. r /\ b e. s))
17	6	adantr 451	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ~P1 a e. M)
18		simprll 738	. . . . . . . . . . . . . . . . . 18 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> r e. Nn )
19		simprrl 740	. . . . . . . . . . . . . . . . . 18 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> a e. r)
20		tfinpw1 4494	. . . . . . . . . . . . . . . . . 18 |- ((r e. Nn /\ a e. r) -> ~P1 a e. Tfin r)
21	18, 19, 20	syl2anc 642	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ~P1 a e. Tfin r)
22		elin 3219	. . . . . . . . . . . . . . . . 17 |- (~P1 a e. (M i^i Tfin r) <-> (~P1 a e. M /\ ~P1 a e. Tfin r))
23	17, 21, 22	sylanbrc 645	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ~P1 a e. (M i^i Tfin r))
24		n0i 3555	. . . . . . . . . . . . . . . 16 |- (~P1 a e. (M i^i Tfin r) -> -. (M i^i Tfin r) = (/))
25	23, 24	syl 15	. . . . . . . . . . . . . . 15 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> -. (M i^i Tfin r) = (/))
26		simpl1l 1006	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> M e. Nn )
27		ne0i 3556	. . . . . . . . . . . . . . . . . 18 |- (a e. r -> r =/= (/))
28	19, 27	syl 15	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> r =/= (/))
29		tfinprop 4489	. . . . . . . . . . . . . . . . . 18 |- ((r e. Nn /\ r =/= (/)) -> ( Tfin r e. Nn /\ E.a e. r ~P1 a e. Tfin r))
30	29	simpld 445	. . . . . . . . . . . . . . . . 17 |- ((r e. Nn /\ r =/= (/)) -> Tfin r e. Nn )
31	18, 28, 30	syl2anc 642	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> Tfin r e. Nn )
32		nndisjeq 4429	. . . . . . . . . . . . . . . 16 |- ((M e. Nn /\ Tfin r e. Nn ) -> ((M i^i Tfin r) = (/) \/ M = Tfin r))
33	26, 31, 32	syl2anc 642	. . . . . . . . . . . . . . 15 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ((M i^i Tfin r) = (/) \/ M = Tfin r))
34		orel1 371	. . . . . . . . . . . . . . 15 |- (-. (M i^i Tfin r) = (/) -> (((M i^i Tfin r) = (/) \/ M = Tfin r) -> M = Tfin r))
35	25, 33, 34	sylc 56	. . . . . . . . . . . . . 14 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> M = Tfin r)
36	10	adantr 451	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ~P1 b e. P)
37		simprlr 739	. . . . . . . . . . . . . . . . . 18 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> s e. Nn )
38		simprrr 741	. . . . . . . . . . . . . . . . . 18 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> b e. s)
39		tfinpw1 4494	. . . . . . . . . . . . . . . . . 18 |- ((s e. Nn /\ b e. s) -> ~P1 b e. Tfin s)
40	37, 38, 39	syl2anc 642	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ~P1 b e. Tfin s)
41		elin 3219	. . . . . . . . . . . . . . . . 17 |- (~P1 b e. (P i^i Tfin s) <-> (~P1 b e. P /\ ~P1 b e. Tfin s))
42	36, 40, 41	sylanbrc 645	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ~P1 b e. (P i^i Tfin s))
43		n0i 3555	. . . . . . . . . . . . . . . 16 |- (~P1 b e. (P i^i Tfin s) -> -. (P i^i Tfin s) = (/))
44	42, 43	syl 15	. . . . . . . . . . . . . . 15 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> -. (P i^i Tfin s) = (/))
45		simpl1r 1007	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> P e. Nn )
46		ne0i 3556	. . . . . . . . . . . . . . . . . 18 |- (b e. s -> s =/= (/))
47	38, 46	syl 15	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> s =/= (/))
48		tfinprop 4489	. . . . . . . . . . . . . . . . . 18 |- ((s e. Nn /\ s =/= (/)) -> ( Tfin s e. Nn /\ E.a e. s ~P1 a e. Tfin s))
49	48	simpld 445	. . . . . . . . . . . . . . . . 17 |- ((s e. Nn /\ s =/= (/)) -> Tfin s e. Nn )
50	37, 47, 49	syl2anc 642	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> Tfin s e. Nn )
51		nndisjeq 4429	. . . . . . . . . . . . . . . 16 |- ((P e. Nn /\ Tfin s e. Nn ) -> ((P i^i Tfin s) = (/) \/ P = Tfin s))
52	45, 50, 51	syl2anc 642	. . . . . . . . . . . . . . 15 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ((P i^i Tfin s) = (/) \/ P = Tfin s))
53		orel1 371	. . . . . . . . . . . . . . 15 |- (-. (P i^i Tfin s) = (/) -> (((P i^i Tfin s) = (/) \/ P = Tfin s) -> P = Tfin s))
54	44, 52, 53	sylc 56	. . . . . . . . . . . . . 14 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> P = Tfin s)
55		tfinltfin 4501	. . . . . . . . . . . . . . . . 17 |- ((r e. Nn /\ s e. Nn ) -> (<<r, s>> e. <fin <-> << Tfin r, Tfin s>> e. <fin ))
56	55	ad2antrl 708	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (<<r, s>> e. <fin <-> << Tfin r, Tfin s>> e. <fin ))
57		opkltfing 4449	. . . . . . . . . . . . . . . . . 18 |- ((r e. Nn /\ s e. Nn ) -> (<<r, s>> e. <fin <-> (r =/= (/) /\ E.t e. Nn s = ((r +o t) +o 1c))))
58	57	ad2antrl 708	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (<<r, s>> e. <fin <-> (r =/= (/) /\ E.t e. Nn s = ((r +o t) +o 1c))))
59		simp2rr 1025	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> b e. s)
60		simp3r 984	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> s = ((r +o t) +o 1c))
61	59, 60	eleqtrd 2429	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> b e. ((r +o t) +o 1c))
62		addcass 4415	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((r +o t) +o 1c) = (r +o (t +o 1c))
63	61, 62	syl6eleq 2443	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> b e. (r +o (t +o 1c)))
64		eladdc 4398	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b e. (r +o (t +o 1c)) <-> E.g e. r E.d e. (t +o 1c)((g i^i d) = (/) /\ b = (g u. d)))
65		0nelsuc 4400	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -. (/) e. (t +o 1c)
66		simprlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> d e. (t +o 1c))
67		eleq1 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (d = (/) -> (d e. (t +o 1c) <-> (/) e. (t +o 1c)))
68	66, 67	syl5ibcom 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (d = (/) -> (/) e. (t +o 1c)))
69	65, 68	mtoi 169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> -. d = (/))
70		df-ne 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (d =/= (/) <-> -. d = (/))
71	69, 70	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> d =/= (/))
72		n0 3559	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (d =/= (/) <-> E.x x e. d)
73		ssun2 3427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- d C_ (g u. d)
74		sseq2 3293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (b = (g u. d) -> (d C_ b <-> d C_ (g u. d)))
75	73, 74	mpbiri 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (b = (g u. d) -> d C_ b)
76	75	sseld 3272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (b = (g u. d) -> (x e. d -> x e. b))
77		disjr 3592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((g i^i d) = (/) <-> A.x e. d -. x e. g)
78		rsp 2674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (A.x e. d -. x e. g -> (x e. d -> -. x e. g))
79	77, 78	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((g i^i d) = (/) -> (x e. d -> -. x e. g))
80	76, 79	anim12ii 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((b = (g u. d) /\ (g i^i d) = (/)) -> (x e. d -> (x e. b /\ -. x e. g)))
81	80	ancoms 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((g i^i d) = (/) /\ b = (g u. d)) -> (x e. d -> (x e. b /\ -. x e. g)))
82	81	ad2antll 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (x e. d -> (x e. b /\ -. x e. g)))
83		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- x e. _V
84	83	snelpw 4115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ({x} e. ~Pb <-> x e. b)
85	83	snelpw 4115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ({x} e. ~Pg <-> x e. g)
86	85	notbii 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (-. {x} e. ~Pg <-> -. x e. g)
87	84, 86	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (({x} e. ~Pb /\ -. {x} e. ~Pg) <-> (x e. b /\ -. x e. g))
88		ssun1 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- g C_ (g u. d)
89		sseq2 3293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (b = (g u. d) -> (g C_ b <-> g C_ (g u. d)))
90	88, 89	mpbiri 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (b = (g u. d) -> g C_ b)
91		sspwb 4118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (g C_ b <-> ~Pg C_ ~Pb)
92	90, 91	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (b = (g u. d) -> ~Pg C_ ~Pb)
93	92	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((g i^i d) = (/) /\ b = (g u. d)) -> ~Pg C_ ~Pb)
94	93	ad2antll 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> ~Pg C_ ~Pb)
95		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (~Pg = ~Pb -> ({x} e. ~Pg <-> {x} e. ~Pb))
96	95	biimprcd 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ({x} e. ~Pb -> (~Pg = ~Pb -> {x} e. ~Pg))
97	96	con3d 125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ({x} e. ~Pb -> (-. {x} e. ~Pg -> -. ~Pg = ~Pb))
98	97	imp 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (({x} e. ~Pb /\ -. {x} e. ~Pg) -> -. ~Pg = ~Pb)
99	98	anim2i 552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((~Pg C_ ~Pb /\ ({x} e. ~Pb /\ -. {x} e. ~Pg)) -> (~Pg C_ ~Pb /\ -. ~Pg = ~Pb))
100		dfpss2 3354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (~Pg C. ~Pb <-> (~Pg C_ ~Pb /\ -. ~Pg = ~Pb))
101	99, 100	sylibr 203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((~Pg C_ ~Pb /\ ({x} e. ~Pb /\ -. {x} e. ~Pg)) -> ~Pg C. ~Pb)
102		simp2ll 1022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> r e. Nn )
103	102	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> r e. Nn )
104		simp2rl 1024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> a e. r)
105	104	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> a e. r)
106		simprll 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> g e. r)
107		nnpweq 4523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((r e. Nn /\ a e. r /\ g e. r) -> E.u e. Nn (~Pa e. u /\ ~Pg e. u))
108	103, 105, 106, 107	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> E.u e. Nn (~Pa e. u /\ ~Pg e. u))
109		simpr2l 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ~Pa e. u)
110		simp3lr 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ~Pa e. N)
111	110	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> ~Pa e. N)
112	111	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ~Pa e. N)
113		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (~Pa e. (u i^i N) <-> (~Pa e. u /\ ~Pa e. N))
114	109, 112, 113	sylanbrc 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ~Pa e. (u i^i N))
115		n0i 3555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (~Pa e. (u i^i N) -> -. (u i^i N) = (/))
116	114, 115	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> -. (u i^i N) = (/))
117		simpr1 961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> u e. Nn )
118		simp12l 1068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> N e. Nn )
119	118	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> N e. Nn )
120		nndisjeq 4429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((u e. Nn /\ N e. Nn ) -> ((u i^i N) = (/) \/ u = N))
121	117, 119, 120	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ((u i^i N) = (/) \/ u = N))
122		orel1 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (-. (u i^i N) = (/) -> (((u i^i N) = (/) \/ u = N) -> u = N))
123	116, 121, 122	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> u = N)
124		simp3rr 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ~Pb e. Q)
125	124	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> ~Pb e. Q)
126	125	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ~Pb e. Q)
127		simp12r 1069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> Q e. Nn )
128	127	ad2antrr 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> Q e. Nn )
129		elunii 3896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((~Pb e. Q /\ Q e. Nn ) -> ~Pb e. U. Nn )
130	126, 128, 129	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ~Pb e. U. Nn )
131		df-fin 4380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- Fin = U. Nn
132	130, 131	syl6eleqr 2444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ~Pb e. Fin )
133		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- b e. _V
134	133	pwex 4329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ~Pb e. _V
135		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- g e. _V
136	135	pwex 4329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ~Pg e. _V
137	134, 136	difex 4107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (~Pb \ ~Pg) e. _V
138		difss 3393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (~Pb \ ~Pg) C_ ~Pb
139		ssfin 4470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((~Pb \ ~Pg) e. _V /\ ~Pb e. Fin /\ (~Pb \ ~Pg) C_ ~Pb) -> (~Pb \ ~Pg) e. Fin )
140	137, 138, 139	mp3an13 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (~Pb e. Fin -> (~Pb \ ~Pg) e. Fin )
141	132, 140	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> (~Pb \ ~Pg) e. Fin )
142		elfin 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((~Pb \ ~Pg) e. Fin <-> E.n e. Nn (~Pb \ ~Pg) e. n)
143	125	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> ~Pb e. Q)
144	143	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ~Pb e. Q)
145		undif1 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((~Pb \ ~Pg) u. ~Pg) = (~Pb u. ~Pg)
146		uncom 3408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((~Pb \ ~Pg) u. ~Pg) = (~Pg u. (~Pb \ ~Pg))
147	145, 146	eqtr3i 2375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (~Pb u. ~Pg) = (~Pg u. (~Pb \ ~Pg))
148		simp23 990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ~Pg C. ~Pb)
149	148	pssssd 3366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ~Pg C_ ~Pb)
150		ssequn2 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (~Pg C_ ~Pb <-> (~Pb u. ~Pg) = ~Pb)
151	149, 150	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (~Pb u. ~Pg) = ~Pb)
152	147, 151	syl5eqr 2399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (~Pg u. (~Pb \ ~Pg)) = ~Pb)
153		simp22r 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ~Pg e. u)
154		simp3r 984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (~Pb \ ~Pg) e. n)
155		disjdif 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (~Pg i^i (~Pb \ ~Pg)) = (/)
156	155	a1i 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (~Pg i^i (~Pb \ ~Pg)) = (/))
157		eladdci 4399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((~Pg e. u /\ (~Pb \ ~Pg) e. n /\ (~Pg i^i (~Pb \ ~Pg)) = (/)) -> (~Pg u. (~Pb \ ~Pg)) e. (u +o n))
158	153, 154, 156, 157	syl3anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (~Pg u. (~Pb \ ~Pg)) e. (u +o n))
159	152, 158	eqeltrrd 2428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ~Pb e. (u +o n))
160		elin 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (~Pb e. (Q i^i (u +o n)) <-> (~Pb e. Q /\ ~Pb e. (u +o n)))
161	144, 159, 160	sylanbrc 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ~Pb e. (Q i^i (u +o n)))
162		n0i 3555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (~Pb e. (Q i^i (u +o n)) -> -. (Q i^i (u +o n)) = (/))
163	161, 162	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> -. (Q i^i (u +o n)) = (/))
164	127	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> Q e. Nn )
165	164	3ad2ant1 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> Q e. Nn )
166		simp21 988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> u e. Nn )
167		simp3l 983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> n e. Nn )
168		nncaddccl 4419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((u e. Nn /\ n e. Nn ) -> (u +o n) e. Nn )
169	166, 167, 168	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (u +o n) e. Nn )
170		nndisjeq 4429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((Q e. Nn /\ (u +o n) e. Nn ) -> ((Q i^i (u +o n)) = (/) \/ Q = (u +o n)))
171	165, 169, 170	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> ((Q i^i (u +o n)) = (/) \/ Q = (u +o n)))
172		orel1 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (-. (Q i^i (u +o n)) = (/) -> (((Q i^i (u +o n)) = (/) \/ Q = (u +o n)) -> Q = (u +o n)))
173	163, 171, 172	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> Q = (u +o n))
174		ne0i 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (~Pg e. u -> u =/= (/))
175	153, 174	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> u =/= (/))
176		df-pss 3261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (~Pg C. ~Pb <-> (~Pg C_ ~Pb /\ ~Pg =/= ~Pb))
177		ssdif0 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (~Pb C_ ~Pg <-> (~Pb \ ~Pg) = (/))
178		eqss 3287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (~Pg = ~Pb <-> (~Pg C_ ~Pb /\ ~Pb C_ ~Pg))
179	178	simplbi2 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (~Pg C_ ~Pb -> (~Pb C_ ~Pg -> ~Pg = ~Pb))
180	177, 179	syl5bir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (~Pg C_ ~Pb -> ((~Pb \ ~Pg) = (/) -> ~Pg = ~Pb))
181	180	necon3d 2554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (~Pg C_ ~Pb -> (~Pg =/= ~Pb -> (~Pb \ ~Pg) =/= (/)))
182	181	imp 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((~Pg C_ ~Pb /\ ~Pg =/= ~Pb) -> (~Pb \ ~Pg) =/= (/))
183	176, 182	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (~Pg C. ~Pb -> (~Pb \ ~Pg) =/= (/))
184	148, 183	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (~Pb \ ~Pg) =/= (/))
185		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (n = 0c -> ((~Pb \ ~Pg) e. n <-> (~Pb \ ~Pg) e. 0c))
186	185	biimpcd 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((~Pb \ ~Pg) e. n -> (n = 0c -> (~Pb \ ~Pg) e. 0c))
187		el0c 4421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((~Pb \ ~Pg) e. 0c <-> (~Pb \ ~Pg) = (/))
188	186, 187	syl6ib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((~Pb \ ~Pg) e. n -> (n = 0c -> (~Pb \ ~Pg) = (/)))
189	188	necon3ad 2552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((~Pb \ ~Pg) e. n -> ((~Pb \ ~Pg) =/= (/) -> -. n = 0c))
190	154, 184, 189	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> -. n = 0c)
191		nnc0suc 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (n e. Nn <-> (n = 0c \/ E.m e. Nn n = (m +o 1c)))
192	167, 191	sylib 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (n = 0c \/ E.m e. Nn n = (m +o 1c)))
193		orel1 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (-. n = 0c -> ((n = 0c \/ E.m e. Nn n = (m +o 1c)) -> E.m e. Nn n = (m +o 1c)))
194	190, 192, 193	sylc 56	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> E.m e. Nn n = (m +o 1c))
195		addceq2 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (n = (m +o 1c) -> (u +o n) = (u +o (m +o 1c)))
196		addcass 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((u +o m) +o 1c) = (u +o (m +o 1c))
197	195, 196	syl6eqr 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (n = (m +o 1c) -> (u +o n) = ((u +o m) +o 1c))
198	197	reximi 2721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (E.m e. Nn n = (m +o 1c) -> E.m e. Nn (u +o n) = ((u +o m) +o 1c))
199	194, 198	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> E.m e. Nn (u +o n) = ((u +o m) +o 1c))
200		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- u e. _V
201		vex 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- n e. _V
202	200, 201	addcex 4394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (u +o n) e. _V
203		opkltfing 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((u e. _V /\ (u +o n) e. _V) -> (<<u, (u +o n)>> e. <fin <-> (u =/= (/) /\ E.m e. Nn (u +o n) = ((u +o m) +o 1c))))
204	200, 202, 203	mp2an 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (<<u, (u +o n)>> e. <fin <-> (u =/= (/) /\ E.m e. Nn (u +o n) = ((u +o m) +o 1c)))
205	175, 199, 204	sylanbrc 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> <<u, (u +o n)>> e. <fin )
206		opkeq2 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (Q = (u +o n) -> <<u, Q>> = <<u, (u +o n)>>)
207	206	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (Q = (u +o n) -> (<<u, Q>> e. <fin <-> <<u, (u +o n)>> e. <fin ))
208	205, 207	syl5ibrcom 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> (Q = (u +o n) -> <<u, Q>> e. <fin ))
209	173, 208	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> <<u, Q>> e. <fin )
210	209	3expa 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) /\ (n e. Nn /\ (~Pb \ ~Pg) e. n)) -> <<u, Q>> e. <fin )
211	210	exp32 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> (n e. Nn -> ((~Pb \ ~Pg) e. n -> <<u, Q>> e. <fin )))
212	211	rexlimdv 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> (E.n e. Nn (~Pb \ ~Pg) e. n -> <<u, Q>> e. <fin ))
213	142, 212	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> ((~Pb \ ~Pg) e. Fin -> <<u, Q>> e. <fin ))
214	141, 213	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> <<u, Q>> e. <fin )
215		opkeq1 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (u = N -> <<u, Q>> = <<N, Q>>)
216	215	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u = N -> (<<u, Q>> e. <fin <-> <<N, Q>> e. <fin ))
217	214, 216	syl5ibcom 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> (u = N -> <<N, Q>> e. <fin ))
218	123, 217	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) /\ (u e. Nn /\ (~Pa e. u /\ ~Pg e. u) /\ ~Pg C. ~Pb)) -> <<N, Q>> e. <fin )
219	218	3exp2 1169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (u e. Nn -> ((~Pa e. u /\ ~Pg e. u) -> (~Pg C. ~Pb -> <<N, Q>> e. <fin ))))
220	219	rexlimdv 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (E.u e. Nn (~Pa e. u /\ ~Pg e. u) -> (~Pg C. ~Pb -> <<N, Q>> e. <fin )))
221	108, 220	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (~Pg C. ~Pb -> <<N, Q>> e. <fin ))
222	101, 221	syl5 28	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> ((~Pg C_ ~Pb /\ ({x} e. ~Pb /\ -. {x} e. ~Pg)) -> <<N, Q>> e. <fin ))
223	94, 222	mpand 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (({x} e. ~Pb /\ -. {x} e. ~Pg) -> <<N, Q>> e. <fin ))
224	87, 223	syl5bir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> ((x e. b /\ -. x e. g) -> <<N, Q>> e. <fin ))
225	82, 224	syld 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (x e. d -> <<N, Q>> e. <fin ))
226	225	exlimdv 1636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (E.x x e. d -> <<N, Q>> e. <fin ))
227	72, 226	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> (d =/= (/) -> <<N, Q>> e. <fin ))
228	71, 227	mpd 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) /\ ((g e. r /\ d e. (t +o 1c)) /\ ((g i^i d) = (/) /\ b = (g u. d)))) -> <<N, Q>> e. <fin )
229	228	exp32 588	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> ((g e. r /\ d e. (t +o 1c)) -> (((g i^i d) = (/) /\ b = (g u. d)) -> <<N, Q>> e. <fin )))
230	229	rexlimdvv 2744	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> (E.g e. r E.d e. (t +o 1c)((g i^i d) = (/) /\ b = (g u. d)) -> <<N, Q>> e. <fin ))
231	64, 230	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> (b e. (r +o (t +o 1c)) -> <<N, Q>> e. <fin ))
232	63, 231	mpd 14	. . . . . . . . . . . . . . . . . . . . 21 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s)) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> <<N, Q>> e. <fin )
233	232	3expa 1151	. . . . . . . . . . . . . . . . . . . 20 |- (((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) /\ (t e. Nn /\ s = ((r +o t) +o 1c))) -> <<N, Q>> e. <fin )
234	233	exp32 588	. . . . . . . . . . . . . . . . . . 19 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (t e. Nn -> (s = ((r +o t) +o 1c) -> <<N, Q>> e. <fin )))
235	234	rexlimdv 2737	. . . . . . . . . . . . . . . . . 18 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (E.t e. Nn s = ((r +o t) +o 1c) -> <<N, Q>> e. <fin ))
236	235	adantld 453	. . . . . . . . . . . . . . . . 17 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ((r =/= (/) /\ E.t e. Nn s = ((r +o t) +o 1c)) -> <<N, Q>> e. <fin ))
237	58, 236	sylbid 206	. . . . . . . . . . . . . . . 16 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (<<r, s>> e. <fin -> <<N, Q>> e. <fin ))
238	56, 237	sylbird 226	. . . . . . . . . . . . . . 15 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (<< Tfin r, Tfin s>> e. <fin -> <<N, Q>> e. <fin ))
239		opkeq12 4061	. . . . . . . . . . . . . . . . 17 |- ((M = Tfin r /\ P = Tfin s) -> <<M, P>> = << Tfin r, Tfin s>>)
240	239	eleq1d 2419	. . . . . . . . . . . . . . . 16 |- ((M = Tfin r /\ P = Tfin s) -> (<<M, P>> e. <fin <-> << Tfin r, Tfin s>> e. <fin ))
241	240	imbi1d 308	. . . . . . . . . . . . . . 15 |- ((M = Tfin r /\ P = Tfin s) -> ((<<M, P>> e. <fin -> <<N, Q>> e. <fin ) <-> (<< Tfin r, Tfin s>> e. <fin -> <<N, Q>> e. <fin )))
242	238, 241	syl5ibrcom 213	. . . . . . . . . . . . . 14 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> ((M = Tfin r /\ P = Tfin s) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin )))
243	35, 54, 242	mp2and 660	. . . . . . . . . . . . 13 |- ((((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) /\ ((r e. Nn /\ s e. Nn ) /\ (a e. r /\ b e. s))) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))
244	243	exp32 588	. . . . . . . . . . . 12 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ((r e. Nn /\ s e. Nn ) -> ((a e. r /\ b e. s) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))))
245	16, 244	syl7 63	. . . . . . . . . . 11 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ((r e. Nn /\ s e. Nn ) -> (((a e. r /\ a e. r) /\ (b e. s /\ b e. s)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))))
246	245	rexlimdvv 2744	. . . . . . . . . 10 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> (E.r e. Nn E.s e. Nn ((a e. r /\ a e. r) /\ (b e. s /\ b e. s)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin )))
247	13, 246	syl5bir 209	. . . . . . . . 9 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> ((E.r e. Nn (a e. r /\ a e. r) /\ E.s e. Nn (b e. s /\ b e. s)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin )))
248	8, 12, 247	mp2and 660	. . . . . . . 8 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ ((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q))) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))
249	248	3expia 1153	. . . . . . 7 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn )) -> (((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin )))
250	249	exlimdvv 1637	. . . . . 6 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn )) -> (E.aE.b((~P1 a e. M /\ ~Pa e. N) /\ (~P1 b e. P /\ ~Pb e. Q)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin )))
251	4, 250	syl5bir 209	. . . . 5 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn )) -> ((E.a(~P1 a e. M /\ ~Pa e. N) /\ E.b(~P1 b e. P /\ ~Pb e. Q)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin )))
252	251	3impia 1148	. . . 4 |- (((M e. Nn /\ P e. Nn ) /\ (N e. Nn /\ Q e. Nn ) /\ (E.a(~P1 a e. M /\ ~Pa e. N) /\ E.b(~P1 b e. P /\ ~Pb e. Q))) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))
253	3, 252	sylbir 204	. . 3 |- (((M e. Nn /\ N e. Nn /\ E.a(~P1 a e. M /\ ~Pa e. N)) /\ (P e. Nn /\ Q e. Nn /\ E.b(~P1 b e. P /\ ~Pb e. Q))) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))
254	1, 2, 253	syl2anb 465	. 2 |- (( Sfin (M, N) /\ Sfin (P, Q)) -> (<<M, P>> e. <fin -> <<N, Q>> e. <fin ))
255	254	imp 418	1 |- ((( Sfin (M, N) /\ Sfin (P, Q)) /\ <<M, P>> e. <fin ) -> <<N, Q>> e. <fin )

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   /\ w3a 934  E.wex 1541   = wceq 1642   e. wcel 1710   =/= wne 2516  A.wral 2614  E.wrex 2615  _Vcvv 2859   \ cdif 3206   u. cun 3207   i^i cin 3208   C_ wss 3257   C. wpss 3258  (/)c0 3550  ~Pcpw 3722  {csn 3737  U.cuni 3891  <<copk 4057  1_cc1c 4134  ~P₁ cpw1 4135   Nn cnnc 4373  0_cc0c 4374   +o cplc 4375   Fin cfin 4376   <_fin cltfin 4433   T_fin ctfin 4435   S_fin wsfin 4438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-tfin 4443  df-sfin 4446

This theorem is referenced by:  sfin111  4536  vfinspsslem1  4550