Metamath Proof Explorer

Theorem cantnfres

Description: The CNF function respects extensions of the domain to a larger ordinal. (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfrescl.d 
|- ( ph -> D e. On )
cantnfrescl.b 
|- ( ph -> B C_ D )
cantnfrescl.x 
|- ( ( ph /\ n e. ( D \ B ) ) -> X = (/) )
cantnfrescl.a 
|- ( ph -> (/) e. A )
cantnfrescl.t 
|- T = dom ( A CNF D )
cantnfres.m 
|- ( ph -> ( n e. B |-> X ) e. S )
Assertion cantnfres 
|- ( ph -> ( ( A CNF B ) ` ( n e. B |-> X ) ) = ( ( A CNF D ) ` ( n e. D |-> X ) ) )

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 cantnfrescl.d 
 |-  ( ph -> D e. On )
5 cantnfrescl.b 
 |-  ( ph -> B C_ D )
6 cantnfrescl.x 
 |-  ( ( ph /\ n e. ( D \ B ) ) -> X = (/) )
7 cantnfrescl.a 
 |-  ( ph -> (/) e. A )
8 cantnfrescl.t 
 |-  T = dom ( A CNF D )
9 cantnfres.m 
 |-  ( ph -> ( n e. B |-> X ) e. S )
10 4 5 6 extmptsuppeq 
 |-  ( ph -> ( ( n e. B |-> X ) supp (/) ) = ( ( n e. D |-> X ) supp (/) ) )
11 oieq2 
 |-  ( ( ( n e. B |-> X ) supp (/) ) = ( ( n e. D |-> X ) supp (/) ) -> OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) = OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) )
12 10 11 syl 
 |-  ( ph -> OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) = OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) )
13 12 fveq1d 
 |-  ( ph -> ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) = ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) )
14 13 3ad2ant1 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) = ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) )
15 14 oveq2d 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) = ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) )
16 suppssdm 
 |-  ( ( n e. B |-> X ) supp (/) ) C_ dom ( n e. B |-> X )
17 eqid 
 |-  ( n e. B |-> X ) = ( n e. B |-> X )
18 17 dmmptss 
 |-  dom ( n e. B |-> X ) C_ B
19 18 a1i 
 |-  ( ph -> dom ( n e. B |-> X ) C_ B )
20 16 19 sstrid 
 |-  ( ph -> ( ( n e. B |-> X ) supp (/) ) C_ B )
21 20 3ad2ant1 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( n e. B |-> X ) supp (/) ) C_ B )
22 eqid 
 |-  OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) = OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) )
23 22 oif 
 |-  OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) : dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) --> ( ( n e. B |-> X ) supp (/) )
24 23 ffvelrni 
 |-  ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) -> ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) e. ( ( n e. B |-> X ) supp (/) ) )
25 24 3ad2ant2 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) e. ( ( n e. B |-> X ) supp (/) ) )
26 21 25 sseldd 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) e. B )
27 26 fvresd 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( ( n e. D |-> X ) |` B ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) = ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) )
28 5 3ad2ant1 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> B C_ D )
29 28 resmptd 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( n e. D |-> X ) |` B ) = ( n e. B |-> X ) )
30 29 fveq1d 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( ( n e. D |-> X ) |` B ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) = ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) )
31 14 fveq2d 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) = ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) )
32 27 30 31 3eqtr3d 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) = ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) )
33 15 32 oveq12d 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) = ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) )
34 33 oveq1d 
 |-  ( ( ph /\ k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) /\ z e. On ) -> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) = ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) )
35 34 mpoeq3dva 
 |-  ( ph -> ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) = ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) )
36 12 dmeqd 
 |-  ( ph -> dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) = dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) )
37 eqid 
 |-  On = On
38 mpoeq12 
 |-  ( ( dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) = dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) /\ On = On ) -> ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) = ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) )
39 36 37 38 sylancl 
 |-  ( ph -> ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) = ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) )
40 35 39 eqtrd 
 |-  ( ph -> ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) = ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) )
41 eqid 
 |-  (/) = (/)
42 seqomeq12 
 |-  ( ( ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) = ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) /\ (/) = (/) ) -> seqom ( ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) )
43 40 41 42 sylancl 
 |-  ( ph -> seqom ( ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) )
44 43 36 fveq12d 
 |-  ( ph -> ( seqom ( ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ) = ( seqom ( ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ) )
45 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
46 1 2 3 22 9 45 cantnfval2 
 |-  ( ph -> ( ( A CNF B ) ` ( n e. B |-> X ) ) = ( seqom ( ( k e. dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. B |-> X ) ` ( OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( ( n e. B |-> X ) supp (/) ) ) ) )
47 eqid 
 |-  OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) = OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) )
48 1 2 3 4 5 6 7 8 cantnfrescl 
 |-  ( ph -> ( ( n e. B |-> X ) e. S <-> ( n e. D |-> X ) e. T ) )
49 9 48 mpbid 
 |-  ( ph -> ( n e. D |-> X ) e. T )
50 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
51 8 2 4 47 49 50 cantnfval2 
 |-  ( ph -> ( ( A CNF D ) ` ( n e. D |-> X ) ) = ( seqom ( ( k e. dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) , z e. On |-> ( ( ( A ^o ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) .o ( ( n e. D |-> X ) ` ( OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( ( n e. D |-> X ) supp (/) ) ) ) )
52 44 46 51 3eqtr4d 
 |-  ( ph -> ( ( A CNF B ) ` ( n e. B |-> X ) ) = ( ( A CNF D ) ` ( n e. D |-> X ) ) )