cantnflem1c

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019) (Proof shortened by AV, 4-Apr-2020)

	Ref	Expression
Hypotheses	cantnfs.s	\|- S = dom ( A CNF B )
	cantnfs.a	\|- ( ph -> A e. On )
	cantnfs.b	\|- ( ph -> B e. On )
	oemapval.t	\|- T = { <. x , y >. \| E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
	oemapval.f	\|- ( ph -> F e. S )
	oemapval.g	\|- ( ph -> G e. S )
	oemapvali.r	\|- ( ph -> F T G )
	oemapvali.x	\|- X = U. { c e. B \| ( F ` c ) e. ( G ` c ) }
	cantnflem1.o	\|- O = OrdIso ( _E , ( G supp (/) ) )
Assertion	cantnflem1c	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( G supp (/) ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	\|- S = dom ( A CNF B )
2		cantnfs.a	\|- ( ph -> A e. On )
3		cantnfs.b	\|- ( ph -> B e. On )
4		oemapval.t	\|- T = { <. x , y >. \| E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5		oemapval.f	\|- ( ph -> F e. S )
6		oemapval.g	\|- ( ph -> G e. S )
7		oemapvali.r	\|- ( ph -> F T G )
8		oemapvali.x	\|- X = U. { c e. B \| ( F ` c ) e. ( G ` c ) }
9		cantnflem1.o	\|- O = OrdIso ( _E , ( G supp (/) ) )
10	3	ad3antrrr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> B e. On )
11		simplr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. B )
12	1 2 3	cantnfs	\|- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
13	6 12	mpbid	\|- ( ph -> ( G : B --> A /\ G finSupp (/) ) )
14	13	simpld	\|- ( ph -> G : B --> A )
15	14	ffnd	\|- ( ph -> G Fn B )
16	15	ad3antrrr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> G Fn B )
17	1 2 3 4 5 6 7 8 9	cantnflem1b	\|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> X C_ ( O ` u ) )
18	17	ad2antrr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> X C_ ( O ` u ) )
19		simprr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. x )
20	1 2 3 4 5 6 7 8	oemapvali	\|- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
21	20	simp1d	\|- ( ph -> X e. B )
22		onelon	\|- ( ( B e. On /\ X e. B ) -> X e. On )
23	3 21 22	syl2anc	\|- ( ph -> X e. On )
24	23	ad3antrrr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> X e. On )
25		onss	\|- ( B e. On -> B C_ On )
26	3 25	syl	\|- ( ph -> B C_ On )
27	26	sselda	\|- ( ( ph /\ x e. B ) -> x e. On )
28	27	ad4ant13	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. On )
29		ontr2	\|- ( ( X e. On /\ x e. On ) -> ( ( X C_ ( O ` u ) /\ ( O ` u ) e. x ) -> X e. x ) )
30	24 28 29	syl2anc	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( X C_ ( O ` u ) /\ ( O ` u ) e. x ) -> X e. x ) )
31	18 19 30	mp2and	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> X e. x )
32		eleq2w	\|- ( w = x -> ( X e. w <-> X e. x ) )
33		fveq2	\|- ( w = x -> ( F ` w ) = ( F ` x ) )
34		fveq2	\|- ( w = x -> ( G ` w ) = ( G ` x ) )
35	33 34	eqeq12d	\|- ( w = x -> ( ( F ` w ) = ( G ` w ) <-> ( F ` x ) = ( G ` x ) ) )
36	32 35	imbi12d	\|- ( w = x -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) )
37	20	simp3d	\|- ( ph -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
38	37	ad3antrrr	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
39	36 38 11	rspcdva	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( X e. x -> ( F ` x ) = ( G ` x ) ) )
40	31 39	mpd	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( F ` x ) = ( G ` x ) )
41		simprl	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( F ` x ) =/= (/) )
42	40 41	eqnetrrd	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( G ` x ) =/= (/) )
43		fvn0elsupp	\|- ( ( ( B e. On /\ x e. B ) /\ ( G Fn B /\ ( G ` x ) =/= (/) ) ) -> x e. ( G supp (/) ) )
44	10 11 16 42 43	syl22anc	\|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( G supp (/) ) )

Metamath Proof Explorer

Theorem cantnflem1c

Proof