Theorem finsschain 15373

Description: A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub 15441 and others.

Assertion

Ref	Expression
finsschain	|- (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) /\ (B e. Fin /\ B C_ U.A)) -> E.z e. A B C_ z)

Distinct variable groups:   x,y,z,A   x,B,y,z

Proof of Theorem finsschain

Step	Hyp	Ref	Expression
1		sseq1 2637	. . . . . 6 |- (b = B -> (b C_ U.A <-> B C_ U.A))
2		sseq1 2637	. . . . . . 7 |- (b = B -> (b C_ z <-> B C_ z))
3	2	rexbidv 2124	. . . . . 6 |- (b = B -> (E.z e. A b C_ z <-> E.z e. A B C_ z))
4	1, 3	imbi12d 688	. . . . 5 |- (b = B -> ((b C_ U.A -> E.z e. A b C_ z) <-> (B C_ U.A -> E.z e. A B C_ z)))
5	4	imbi2d 674	. . . 4 |- (b = B -> (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)) <-> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (B C_ U.A -> E.z e. A B C_ z))))
6		isfi 5441	. . . . 5 |- (b e. Fin <-> E.k e. om b ~~ k)
7		breq2 3342	. . . . . . . . . 10 |- (n = (/) -> (b ~~ n <-> b ~~ (/)))
8	7	imbi1d 675	. . . . . . . . 9 |- (n = (/) -> ((b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> (b ~~ (/) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
9	8	albidv 1656	. . . . . . . 8 |- (n = (/) -> (A.b(b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> A.b(b ~~ (/) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
10		breq2 3342	. . . . . . . . . 10 |- (n = j -> (b ~~ n <-> b ~~ j))
11	10	imbi1d 675	. . . . . . . . 9 |- (n = j -> ((b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> (b ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
12	11	albidv 1656	. . . . . . . 8 |- (n = j -> (A.b(b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> A.b(b ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
13		breq2 3342	. . . . . . . . . 10 |- (n = suc j -> (b ~~ n <-> b ~~ suc j))
14	13	imbi1d 675	. . . . . . . . 9 |- (n = suc j -> ((b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> (b ~~ suc j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
15	14	albidv 1656	. . . . . . . 8 |- (n = suc j -> (A.b(b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> A.b(b ~~ suc j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
16		breq2 3342	. . . . . . . . . 10 |- (n = k -> (b ~~ n <-> b ~~ k))
17	16	imbi1d 675	. . . . . . . . 9 |- (n = k -> ((b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> (b ~~ k -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
18	17	albidv 1656	. . . . . . . 8 |- (n = k -> (A.b(b ~~ n -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> A.b(b ~~ k -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
19		en0 5482	. . . . . . . . . 10 |- (b ~~ (/) <-> b = (/))
20		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (b = (/) -> (b C_ z <-> (/) C_ z))
21	20	rexbidv 2124	. . . . . . . . . . . . . . 15 |- (b = (/) -> (E.z e. A b C_ z <-> E.z e. A (/) C_ z))
22		0ss 2900	. . . . . . . . . . . . . . . 16 |- (/) C_ x
23		sseq2 2639	. . . . . . . . . . . . . . . . 17 |- (z = x -> ((/) C_ z <-> (/) C_ x))
24	23	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- ((x e. A /\ (/) C_ x) -> E.z e. A (/) C_ z)
25	22, 24	mpan2 760	. . . . . . . . . . . . . . 15 |- (x e. A -> E.z e. A (/) C_ z)
26	21, 25	syl5bir 227	. . . . . . . . . . . . . 14 |- (b = (/) -> (x e. A -> E.z e. A b C_ z))
27	26	19.23adv 1584	. . . . . . . . . . . . 13 |- (b = (/) -> (E.x x e. A -> E.z e. A b C_ z))
28		n0 2884	. . . . . . . . . . . . 13 |- (A =/= (/) <-> E.x x e. A)
29	27, 28	syl5ib 223	. . . . . . . . . . . 12 |- (b = (/) -> (A =/= (/) -> E.z e. A b C_ z))
30	29	a1dd 53	. . . . . . . . . . 11 |- (b = (/) -> (A =/= (/) -> (b C_ U.A -> E.z e. A b C_ z)))
31	30	adantrd 427	. . . . . . . . . 10 |- (b = (/) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))
32	19, 31	sylbi 216	. . . . . . . . 9 |- (b ~~ (/) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))
33	32	ax-gen 1305	. . . . . . . 8 |- A.b(b ~~ (/) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))
34		f1of1 4634	. . . . . . . . . . . . . . . . . . . . 21 |- (`'f:suc j-1-1-onto->b -> `'f:suc j-1-1->b)
35		sssucid 3742	. . . . . . . . . . . . . . . . . . . . . 22 |- j C_ suc j
36		f1ores 4654	. . . . . . . . . . . . . . . . . . . . . 22 |- ((`'f:suc j-1-1->b /\ j C_ suc j) -> (`'f |` j):j-1-1-onto->(`'f"j))
37	35, 36	mpan2 760	. . . . . . . . . . . . . . . . . . . . 21 |- (`'f:suc j-1-1->b -> (`'f |` j):j-1-1-onto->(`'f"j))
38	34, 37	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (`'f:suc j-1-1-onto->b -> (`'f |` j):j-1-1-onto->(`'f"j))
39	38	ad2antlr 441	. . . . . . . . . . . . . . . . . . 19 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (`'f |` j):j-1-1-onto->(`'f"j))
40		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- j e. _V
41	40	f1oen 5457	. . . . . . . . . . . . . . . . . . 19 |- ((`'f |` j):j-1-1-onto->(`'f"j) -> j ~~ (`'f"j))
42		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
43	42	cnvex 4425	. . . . . . . . . . . . . . . . . . . . 21 |- `'f e. _V
44		imaexg 4279	. . . . . . . . . . . . . . . . . . . . 21 |- (`'f e. _V -> (`'f"j) e. _V)
45	43, 44	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (`'f"j) e. _V
46	45	ensym 5471	. . . . . . . . . . . . . . . . . . 19 |- (j ~~ (`'f"j) -> (`'f"j) ~~ j)
47	39, 41, 46	3syl 24	. . . . . . . . . . . . . . . . . 18 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (`'f"j) ~~ j)
48		simprr 451	. . . . . . . . . . . . . . . . . . . 20 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))
49		imassrn 4278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'f"j) C_ ran `' f
50	49	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (`'f:suc j-1-1-onto->b -> (`'f"j) C_ ran `' f)
51		f1ofo 4643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'f:suc j-1-1-onto->b -> `'f:suc j-onto->b)
52		forn 4620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (`'f:suc j-onto->b -> ran `' f = b)
53	51, 52	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (`'f:suc j-1-1-onto->b -> ran `' f = b)
54	50, 53	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (`'f:suc j-1-1-onto->b -> (`'f"j) C_ b)
55	54	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (`'f"j) C_ b)
56		simprl 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> b C_ U.A)
57	55, 56	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . 22 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (`'f"j) C_ U.A)
58		f1of 4635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (`'f:suc j-1-1-onto->b -> `'f:suc j-->b)
59	40	sucid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- j e. suc j
60		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((`'f:suc j-->b /\ j e. suc j) -> (`'f` j) e. b)
61	59, 60	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (`'f:suc j-->b -> (`'f` j) e. b)
62	58, 61	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'f:suc j-1-1-onto->b -> (`'f` j) e. b)
63	62	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (`'f` j) e. b)
64	56, 63	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (`'f` j) e. U.A)
65		eluni2 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((`'f` j) e. U.A <-> E.t e. A (`'f` j) e. t)
66	64, 65	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> E.t e. A (`'f` j) e. t)
67		snssi 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((`'f` j) e. t -> {(`'f` j)} C_ t)
68	67	reximi 2198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.t e. A (`'f` j) e. t -> E.t e. A {(`'f` j)} C_ t)
69	66, 68	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> E.t e. A {(`'f` j)} C_ t)
70		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = t -> (x C_ y <-> t C_ y))
71		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = t -> (y C_ x <-> y C_ t))
72	70, 71	orbi12d 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = t -> ((x C_ y \/ y C_ x) <-> (t C_ y \/ y C_ t)))
73		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = w -> (t C_ y <-> t C_ w))
74		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = w -> (y C_ t <-> w C_ t))
75	73, 74	orbi12d 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y = w -> ((t C_ y \/ y C_ t) <-> (t C_ w \/ w C_ t)))
76	72, 75	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((t e. A /\ w e. A) -> (A.x e. A A.y e. A (x C_ y \/ y C_ x) -> (t C_ w \/ w C_ t)))
77	76	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (A.x e. A A.y e. A (x C_ y \/ y C_ x) -> (t C_ w \/ w C_ t)))
78		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> w e. A)
79	78	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> w e. A)
80		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (`'f"j) C_ w)
81	80	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> (`'f"j) C_ w)
82		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> {(`'f` j)} C_ t)
83	82	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> {(`'f` j)} C_ t)
84		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> t C_ w)
85	83, 84	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> {(`'f` j)} C_ w)
86	81, 85	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> ((`'f"j) C_ w /\ {(`'f` j)} C_ w))
87		unss 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((`'f"j) C_ w /\ {(`'f` j)} C_ w) <-> ((`'f"j) u. {(`'f` j)}) C_ w)
88	86, 87	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> ((`'f"j) u. {(`'f` j)}) C_ w)
89		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (z = w -> (((`'f"j) u. {(`'f` j)}) C_ z <-> ((`'f"j) u. {(`'f` j)}) C_ w))
90	89	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((w e. A /\ ((`'f"j) u. {(`'f` j)}) C_ w) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)
91	79, 88, 90	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ t C_ w) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)
92	91	exp58 15342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (t C_ w -> (A =/= (/) -> (b C_ U.A -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)))))
93		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> t e. A)
94	93	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> t e. A)
95		simplrr 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) -> (`'f"j) C_ w)
96		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) -> w C_ t)
97	95, 96	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) -> (`'f"j) C_ t)
98		simpllr 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) -> {(`'f` j)} C_ t)
99	97, 98	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) -> ((`'f"j) C_ t /\ {(`'f` j)} C_ t))
100	99	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> ((`'f"j) C_ t /\ {(`'f` j)} C_ t))
101		unss 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((`'f"j) C_ t /\ {(`'f` j)} C_ t) <-> ((`'f"j) u. {(`'f` j)}) C_ t)
102	100, 101	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> ((`'f"j) u. {(`'f` j)}) C_ t)
103		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (z = t -> (((`'f"j) u. {(`'f` j)}) C_ z <-> ((`'f"j) u. {(`'f` j)}) C_ t))
104	103	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((t e. A /\ ((`'f"j) u. {(`'f` j)}) C_ t) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)
105	94, 102, 104	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) /\ w C_ t) /\ ((A =/= (/) /\ b C_ U.A) /\ (j e. om /\ `'f:suc j-1-1-onto->b))) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)
106	105	exp58 15342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (w C_ t -> (A =/= (/) -> (b C_ U.A -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)))))
107	92, 106	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> ((t C_ w \/ w C_ t) -> (A =/= (/) -> (b C_ U.A -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)))))
108	77, 107	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (A.x e. A A.y e. A (x C_ y \/ y C_ x) -> (A =/= (/) -> (b C_ U.A -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)))))
109	108	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (A =/= (/) -> (A.x e. A A.y e. A (x C_ y \/ y C_ x) -> (b C_ U.A -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)))))
110	109	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z))))
111	110	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> (b C_ U.A -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((j e. om /\ `'f:suc j-1-1-onto->b) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z))))
112	111	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((j e. om /\ `'f:suc j-1-1-onto->b) -> (b C_ U.A -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w)) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z))))
113	112	imp42 396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z)
114		f1ofn 4636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (`'f:suc j-1-1-onto->b -> `'f Fn suc j)
115	114	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((j e. om /\ `'f:suc j-1-1-onto->b) -> `'f Fn suc j)
116	115	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> `'f Fn suc j)
117	59	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> j e. suc j)
118		fnsnfv 4728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((`'f Fn suc j /\ j e. suc j) -> {(`'f` j)} = (`'f"{j}))
119	116, 117, 118	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> {(`'f` j)} = (`'f"{j}))
120	119	uneq2d 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> ((`'f"j) u. {(`'f` j)}) = ((`'f"j) u. (`'f"{j})))
121		df-suc 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- suc j = (j u. {j})
122	121	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (`'f"suc j) = (`'f"(j u. {j}))
123		imaundi 4328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (`'f"(j u. {j})) = ((`'f"j) u. (`'f"{j}))
124	122, 123	eqtr2i 1909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((`'f"j) u. (`'f"{j})) = (`'f"suc j)
125	120, 124	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> ((`'f"j) u. {(`'f` j)}) = (`'f"suc j))
126		foima 4622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'f:suc j-onto->b -> (`'f"suc j) = b)
127	51, 126	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (`'f:suc j-1-1-onto->b -> (`'f"suc j) = b)
128	127	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((j e. om /\ `'f:suc j-1-1-onto->b) -> (`'f"suc j) = b)
129	128	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> (`'f"suc j) = b)
130	125, 129	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> ((`'f"j) u. {(`'f` j)}) = b)
131	130	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> (((`'f"j) u. {(`'f` j)}) C_ z <-> b C_ z))
132	131	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> (E.z e. A ((`'f"j) u. {(`'f` j)}) C_ z <-> E.z e. A b C_ z))
133	113, 132	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) /\ ((t e. A /\ {(`'f` j)} C_ t) /\ (w e. A /\ (`'f"j) C_ w))) -> E.z e. A b C_ z)
134	133	exp512 15345	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (t e. A -> ({(`'f` j)} C_ t -> (w e. A -> ((`'f"j) C_ w -> E.z e. A b C_ z)))))
135	134	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (E.t e. A {(`'f` j)} C_ t -> (w e. A -> ((`'f"j) C_ w -> E.z e. A b C_ z))))
136	69, 135	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (w e. A -> ((`'f"j) C_ w -> E.z e. A b C_ z)))
137	136	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (E.w e. A (`'f"j) C_ w -> E.z e. A b C_ z))
138		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = w -> ((`'f"j) C_ z <-> (`'f"j) C_ w))
139	138	cbvrexv 2281	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.z e. A (`'f"j) C_ z <-> E.w e. A (`'f"j) C_ w)
140	137, 139	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (E.z e. A (`'f"j) C_ z -> E.z e. A b C_ z))
141	140	imim2d 28	. . . . . . . . . . . . . . . . . . . . . 22 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z) -> ((`'f"j) C_ U.A -> E.z e. A b C_ z)))
142	57, 141	mpid 58	. . . . . . . . . . . . . . . . . . . . 21 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z) -> E.z e. A b C_ z))
143	142	imim2d 28	. . . . . . . . . . . . . . . . . . . 20 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z)) -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> E.z e. A b C_ z)))
144	48, 143	mpid 58	. . . . . . . . . . . . . . . . . . 19 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z)) -> E.z e. A b C_ z))
145	144	imim2d 28	. . . . . . . . . . . . . . . . . 18 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (((`'f"j) ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z))) -> ((`'f"j) ~~ j -> E.z e. A b C_ z)))
146	47, 145	mpid 58	. . . . . . . . . . . . . . . . 17 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (((`'f"j) ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z))) -> E.z e. A b C_ z))
147		breq1 3341	. . . . . . . . . . . . . . . . . . 19 |- (c = (`'f"j) -> (c ~~ j <-> (`'f"j) ~~ j))
148		sseq1 2637	. . . . . . . . . . . . . . . . . . . . 21 |- (c = (`'f"j) -> (c C_ U.A <-> (`'f"j) C_ U.A))
149		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . 22 |- (c = (`'f"j) -> (c C_ z <-> (`'f"j) C_ z))
150	149	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . 21 |- (c = (`'f"j) -> (E.z e. A c C_ z <-> E.z e. A (`'f"j) C_ z))
151	148, 150	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (c = (`'f"j) -> ((c C_ U.A -> E.z e. A c C_ z) <-> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z)))
152	151	imbi2d 674	. . . . . . . . . . . . . . . . . . 19 |- (c = (`'f"j) -> (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z)) <-> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z))))
153	147, 152	imbi12d 688	. . . . . . . . . . . . . . . . . 18 |- (c = (`'f"j) -> ((c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) <-> ((`'f"j) ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z)))))
154	45, 153	cla4v 2370	. . . . . . . . . . . . . . . . 17 |- (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> ((`'f"j) ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> ((`'f"j) C_ U.A -> E.z e. A (`'f"j) C_ z))))
155	146, 154	syl5 20	. . . . . . . . . . . . . . . 16 |- (((j e. om /\ `'f:suc j-1-1-onto->b) /\ (b C_ U.A /\ (A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)))) -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> E.z e. A b C_ z))
156	155	exp43 415	. . . . . . . . . . . . . . 15 |- (j e. om -> (`'f:suc j-1-1-onto->b -> (b C_ U.A -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> E.z e. A b C_ z)))))
157		f1ocnv 4651	. . . . . . . . . . . . . . 15 |- (f:b-1-1-onto->suc j -> `'f:suc j-1-1-onto->b)
158	156, 157	syl5 20	. . . . . . . . . . . . . 14 |- (j e. om -> (f:b-1-1-onto->suc j -> (b C_ U.A -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> E.z e. A b C_ z)))))
159	158	19.23adv 1584	. . . . . . . . . . . . 13 |- (j e. om -> (E.f f:b-1-1-onto->suc j -> (b C_ U.A -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> E.z e. A b C_ z)))))
160	40	sucex 3892	. . . . . . . . . . . . . 14 |- suc j e. _V
161	160	bren 5436	. . . . . . . . . . . . 13 |- (b ~~ suc j <-> E.f f:b-1-1-onto->suc j)
162	159, 161	syl5ib 223	. . . . . . . . . . . 12 |- (j e. om -> (b ~~ suc j -> (b C_ U.A -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> E.z e. A b C_ z)))))
163	162	com23 36	. . . . . . . . . . 11 |- (j e. om -> (b C_ U.A -> (b ~~ suc j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> E.z e. A b C_ z)))))
164	163	com25 48	. . . . . . . . . 10 |- (j e. om -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> (b ~~ suc j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
165	164	19.21adv 1666	. . . . . . . . 9 |- (j e. om -> (A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))) -> A.b(b ~~ suc j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
166		breq1 3341	. . . . . . . . . . 11 |- (b = c -> (b ~~ j <-> c ~~ j))
167		sseq1 2637	. . . . . . . . . . . . 13 |- (b = c -> (b C_ U.A <-> c C_ U.A))
168		sseq1 2637	. . . . . . . . . . . . . 14 |- (b = c -> (b C_ z <-> c C_ z))
169	168	rexbidv 2124	. . . . . . . . . . . . 13 |- (b = c -> (E.z e. A b C_ z <-> E.z e. A c C_ z))
170	167, 169	imbi12d 688	. . . . . . . . . . . 12 |- (b = c -> ((b C_ U.A -> E.z e. A b C_ z) <-> (c C_ U.A -> E.z e. A c C_ z)))
171	170	imbi2d 674	. . . . . . . . . . 11 |- (b = c -> (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)) <-> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))))
172	166, 171	imbi12d 688	. . . . . . . . . 10 |- (b = c -> ((b ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> (c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z)))))
173	172	cbvalv 1696	. . . . . . . . 9 |- (A.b(b ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) <-> A.c(c ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (c C_ U.A -> E.z e. A c C_ z))))
174	165, 173	syl5ib 223	. . . . . . . 8 |- (j e. om -> (A.b(b ~~ j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))) -> A.b(b ~~ suc j -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))))
175	9, 12, 15, 18, 33, 174	finds 3979	. . . . . . 7 |- (k e. om -> A.b(b ~~ k -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))))
176	175	19.21bi 1408	. . . . . 6 |- (k e. om -> (b ~~ k -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z))))
177	176	r19.23aiv 2211	. . . . 5 |- (E.k e. om b ~~ k -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))
178	6, 177	sylbi 216	. . . 4 |- (b e. Fin -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (b C_ U.A -> E.z e. A b C_ z)))
179	5, 178	vtoclga 2352	. . 3 |- (B e. Fin -> ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (B C_ U.A -> E.z e. A B C_ z)))
180	179	com12 14	. 2 |- ((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) -> (B e. Fin -> (B C_ U.A -> E.z e. A B C_ z)))
181	180	imp32 390	1 |- (((A =/= (/) /\ A.x e. A A.y e. A (x C_ y \/ y C_ x)) /\ (B e. Fin /\ B C_ U.A)) -> E.z e. A B C_ z)

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177   class class class wbr 3338  suc csuc 3659  omcom 3949  `'ccnv 3985  ran crn 3987   |` cres 3988  "cima 3989   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423  Fincfn 5426

This theorem is referenced by:  alexsublem2 15438

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-er 5318  df-en 5427  df-fin 5430

Copyright terms: Public domain