Metamath Proof Explorer


Theorem cnfcomlem

Description: Lemma for cnfcom . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses cnfcom.s โŠข ๐‘† = dom ( ฯ‰ CNF ๐ด )
cnfcom.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
cnfcom.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ ( ฯ‰ โ†‘o ๐ด ) )
cnfcom.f โŠข ๐น = ( โ—ก ( ฯ‰ CNF ๐ด ) โ€˜ ๐ต )
cnfcom.g โŠข ๐บ = OrdIso ( E , ( ๐น supp โˆ… ) )
cnfcom.h โŠข ๐ป = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ๐‘€ +o ๐‘ง ) ) , โˆ… )
cnfcom.t โŠข ๐‘‡ = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) , โˆ… )
cnfcom.m โŠข ๐‘€ = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) )
cnfcom.k โŠข ๐พ = ( ( ๐‘ฅ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฅ ) ) โˆช โ—ก ( ๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฅ ) ) )
cnfcom.1 โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ dom ๐บ )
cnfcom.2 โŠข ( ๐œ‘ โ†’ ๐‘‚ โˆˆ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) )
cnfcom.3 โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ ๐ผ ) : ( ๐ป โ€˜ ๐ผ ) โ€“1-1-ontoโ†’ ๐‘‚ )
Assertion cnfcomlem ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ๐ป โ€˜ suc ๐ผ ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )

Proof

Step Hyp Ref Expression
1 cnfcom.s โŠข ๐‘† = dom ( ฯ‰ CNF ๐ด )
2 cnfcom.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
3 cnfcom.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ ( ฯ‰ โ†‘o ๐ด ) )
4 cnfcom.f โŠข ๐น = ( โ—ก ( ฯ‰ CNF ๐ด ) โ€˜ ๐ต )
5 cnfcom.g โŠข ๐บ = OrdIso ( E , ( ๐น supp โˆ… ) )
6 cnfcom.h โŠข ๐ป = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ๐‘€ +o ๐‘ง ) ) , โˆ… )
7 cnfcom.t โŠข ๐‘‡ = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) , โˆ… )
8 cnfcom.m โŠข ๐‘€ = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) )
9 cnfcom.k โŠข ๐พ = ( ( ๐‘ฅ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฅ ) ) โˆช โ—ก ( ๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฅ ) ) )
10 cnfcom.1 โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ dom ๐บ )
11 cnfcom.2 โŠข ( ๐œ‘ โ†’ ๐‘‚ โˆˆ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) )
12 cnfcom.3 โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ ๐ผ ) : ( ๐ป โ€˜ ๐ผ ) โ€“1-1-ontoโ†’ ๐‘‚ )
13 omelon โŠข ฯ‰ โˆˆ On
14 suppssdm โŠข ( ๐น supp โˆ… ) โŠ† dom ๐น
15 13 a1i โŠข ( ๐œ‘ โ†’ ฯ‰ โˆˆ On )
16 1 15 2 cantnff1o โŠข ( ๐œ‘ โ†’ ( ฯ‰ CNF ๐ด ) : ๐‘† โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐ด ) )
17 f1ocnv โŠข ( ( ฯ‰ CNF ๐ด ) : ๐‘† โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐ด ) โ†’ โ—ก ( ฯ‰ CNF ๐ด ) : ( ฯ‰ โ†‘o ๐ด ) โ€“1-1-ontoโ†’ ๐‘† )
18 f1of โŠข ( โ—ก ( ฯ‰ CNF ๐ด ) : ( ฯ‰ โ†‘o ๐ด ) โ€“1-1-ontoโ†’ ๐‘† โ†’ โ—ก ( ฯ‰ CNF ๐ด ) : ( ฯ‰ โ†‘o ๐ด ) โŸถ ๐‘† )
19 16 17 18 3syl โŠข ( ๐œ‘ โ†’ โ—ก ( ฯ‰ CNF ๐ด ) : ( ฯ‰ โ†‘o ๐ด ) โŸถ ๐‘† )
20 19 3 ffvelrnd โŠข ( ๐œ‘ โ†’ ( โ—ก ( ฯ‰ CNF ๐ด ) โ€˜ ๐ต ) โˆˆ ๐‘† )
21 4 20 eqeltrid โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ๐‘† )
22 1 15 2 cantnfs โŠข ( ๐œ‘ โ†’ ( ๐น โˆˆ ๐‘† โ†” ( ๐น : ๐ด โŸถ ฯ‰ โˆง ๐น finSupp โˆ… ) ) )
23 21 22 mpbid โŠข ( ๐œ‘ โ†’ ( ๐น : ๐ด โŸถ ฯ‰ โˆง ๐น finSupp โˆ… ) )
24 23 simpld โŠข ( ๐œ‘ โ†’ ๐น : ๐ด โŸถ ฯ‰ )
25 14 24 fssdm โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โŠ† ๐ด )
26 5 oif โŠข ๐บ : dom ๐บ โŸถ ( ๐น supp โˆ… )
27 26 ffvelrni โŠข ( ๐ผ โˆˆ dom ๐บ โ†’ ( ๐บ โ€˜ ๐ผ ) โˆˆ ( ๐น supp โˆ… ) )
28 10 27 syl โŠข ( ๐œ‘ โ†’ ( ๐บ โ€˜ ๐ผ ) โˆˆ ( ๐น supp โˆ… ) )
29 25 28 sseldd โŠข ( ๐œ‘ โ†’ ( ๐บ โ€˜ ๐ผ ) โˆˆ ๐ด )
30 onelon โŠข ( ( ๐ด โˆˆ On โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ ๐ด ) โ†’ ( ๐บ โ€˜ ๐ผ ) โˆˆ On )
31 2 29 30 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐บ โ€˜ ๐ผ ) โˆˆ On )
32 oecl โŠข ( ( ฯ‰ โˆˆ On โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On ) โ†’ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On )
33 13 31 32 sylancr โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On )
34 24 29 ffvelrnd โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ ฯ‰ )
35 nnon โŠข ( ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ ฯ‰ โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On )
36 34 35 syl โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On )
37 omcl โŠข ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On โˆง ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On ) โ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โˆˆ On )
38 33 36 37 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โˆˆ On )
39 1 15 2 5 21 cantnfcl โŠข ( ๐œ‘ โ†’ ( E We ( ๐น supp โˆ… ) โˆง dom ๐บ โˆˆ ฯ‰ ) )
40 39 simprd โŠข ( ๐œ‘ โ†’ dom ๐บ โˆˆ ฯ‰ )
41 elnn โŠข ( ( ๐ผ โˆˆ dom ๐บ โˆง dom ๐บ โˆˆ ฯ‰ ) โ†’ ๐ผ โˆˆ ฯ‰ )
42 10 40 41 syl2anc โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ ฯ‰ )
43 6 cantnfvalf โŠข ๐ป : ฯ‰ โŸถ On
44 43 ffvelrni โŠข ( ๐ผ โˆˆ ฯ‰ โ†’ ( ๐ป โ€˜ ๐ผ ) โˆˆ On )
45 42 44 syl โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ ๐ผ ) โˆˆ On )
46 eqid โŠข ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) = ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) )
47 46 oacomf1o โŠข ( ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โˆˆ On โˆง ( ๐ป โ€˜ ๐ผ ) โˆˆ On ) โ†’ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) : ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) )
48 38 45 47 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) : ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) )
49 7 seqomsuc โŠข ( ๐ผ โˆˆ ฯ‰ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) = ( ๐ผ ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) ( ๐‘‡ โ€˜ ๐ผ ) ) )
50 42 49 syl โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) = ( ๐ผ ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) ( ๐‘‡ โ€˜ ๐ผ ) ) )
51 nfcv โŠข โ„ฒ ๐‘ข ๐พ
52 nfcv โŠข โ„ฒ ๐‘ฃ ๐พ
53 nfcv โŠข โ„ฒ ๐‘˜ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) )
54 nfcv โŠข โ„ฒ ๐‘“ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) )
55 oveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( dom ๐‘“ +o ๐‘ฅ ) = ( dom ๐‘“ +o ๐‘ฆ ) )
56 55 cbvmptv โŠข ( ๐‘ฅ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฅ ) ) = ( ๐‘ฆ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฆ ) )
57 simpl โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ๐‘˜ = ๐‘ข )
58 57 fveq2d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐บ โ€˜ ๐‘˜ ) = ( ๐บ โ€˜ ๐‘ข ) )
59 58 oveq2d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) = ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) )
60 58 fveq2d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) = ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) )
61 59 60 oveq12d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) )
62 8 61 eqtrid โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ๐‘€ = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) )
63 simpr โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ๐‘“ = ๐‘ฃ )
64 63 dmeqd โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ dom ๐‘“ = dom ๐‘ฃ )
65 64 oveq1d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( dom ๐‘“ +o ๐‘ฆ ) = ( dom ๐‘ฃ +o ๐‘ฆ ) )
66 62 65 mpteq12dv โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐‘ฆ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฆ ) ) = ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) )
67 56 66 eqtrid โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐‘ฅ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฅ ) ) = ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) )
68 oveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘€ +o ๐‘ฅ ) = ( ๐‘€ +o ๐‘ฆ ) )
69 68 cbvmptv โŠข ( ๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฅ ) ) = ( ๐‘ฆ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฆ ) )
70 62 oveq1d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐‘€ +o ๐‘ฆ ) = ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) )
71 64 70 mpteq12dv โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐‘ฆ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฆ ) ) = ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) )
72 69 71 eqtrid โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฅ ) ) = ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) )
73 72 cnveqd โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ โ—ก ( ๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฅ ) ) = โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) )
74 67 73 uneq12d โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ( ( ๐‘ฅ โˆˆ ๐‘€ โ†ฆ ( dom ๐‘“ +o ๐‘ฅ ) ) โˆช โ—ก ( ๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ ( ๐‘€ +o ๐‘ฅ ) ) ) = ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) ) )
75 9 74 eqtrid โŠข ( ( ๐‘˜ = ๐‘ข โˆง ๐‘“ = ๐‘ฃ ) โ†’ ๐พ = ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) ) )
76 51 52 53 54 75 cbvmpo โŠข ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) = ( ๐‘ข โˆˆ V , ๐‘ฃ โˆˆ V โ†ฆ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) ) )
77 76 a1i โŠข ( ๐œ‘ โ†’ ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) = ( ๐‘ข โˆˆ V , ๐‘ฃ โˆˆ V โ†ฆ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) ) ) )
78 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ๐‘ข = ๐ผ )
79 78 fveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ๐บ โ€˜ ๐‘ข ) = ( ๐บ โ€˜ ๐ผ ) )
80 79 oveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) = ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) )
81 79 fveq2d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) = ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) )
82 80 81 oveq12d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )
83 simpr โŠข ( ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) โ†’ ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) )
84 83 dmeqd โŠข ( ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) โ†’ dom ๐‘ฃ = dom ( ๐‘‡ โ€˜ ๐ผ ) )
85 f1odm โŠข ( ( ๐‘‡ โ€˜ ๐ผ ) : ( ๐ป โ€˜ ๐ผ ) โ€“1-1-ontoโ†’ ๐‘‚ โ†’ dom ( ๐‘‡ โ€˜ ๐ผ ) = ( ๐ป โ€˜ ๐ผ ) )
86 12 85 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘‡ โ€˜ ๐ผ ) = ( ๐ป โ€˜ ๐ผ ) )
87 84 86 sylan9eqr โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ dom ๐‘ฃ = ( ๐ป โ€˜ ๐ผ ) )
88 87 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( dom ๐‘ฃ +o ๐‘ฆ ) = ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) )
89 82 88 mpteq12dv โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) = ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) )
90 82 oveq1d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) = ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) )
91 87 90 mpteq12dv โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) = ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) )
92 91 cnveqd โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) = โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) )
93 89 92 uneq12d โŠข ( ( ๐œ‘ โˆง ( ๐‘ข = ๐ผ โˆง ๐‘ฃ = ( ๐‘‡ โ€˜ ๐ผ ) ) ) โ†’ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) โ†ฆ ( dom ๐‘ฃ +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ dom ๐‘ฃ โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘ข ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘ข ) ) ) +o ๐‘ฆ ) ) ) = ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) )
94 10 elexd โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ V )
95 fvexd โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ ๐ผ ) โˆˆ V )
96 ovex โŠข ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โˆˆ V
97 96 mptex โŠข ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆˆ V
98 fvex โŠข ( ๐ป โ€˜ ๐ผ ) โˆˆ V
99 98 mptex โŠข ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) โˆˆ V
100 99 cnvex โŠข โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) โˆˆ V
101 97 100 unex โŠข ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) โˆˆ V
102 101 a1i โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) โˆˆ V )
103 77 93 94 95 102 ovmpod โŠข ( ๐œ‘ โ†’ ( ๐ผ ( ๐‘˜ โˆˆ V , ๐‘“ โˆˆ V โ†ฆ ๐พ ) ( ๐‘‡ โ€˜ ๐ผ ) ) = ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) )
104 50 103 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) = ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) )
105 104 f1oeq1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) โ†” ( ( ๐‘ฆ โˆˆ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†ฆ ( ( ๐ป โ€˜ ๐ผ ) +o ๐‘ฆ ) ) โˆช โ—ก ( ๐‘ฆ โˆˆ ( ๐ป โ€˜ ๐ผ ) โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ๐‘ฆ ) ) ) : ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) ) )
106 48 105 mpbird โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) )
107 13 a1i โŠข ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โ†’ ฯ‰ โˆˆ On )
108 simpl โŠข ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โ†’ ๐ด โˆˆ On )
109 simpr โŠข ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โ†’ ๐น โˆˆ ๐‘† )
110 8 oveq1i โŠข ( ๐‘€ +o ๐‘ง ) = ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง )
111 110 a1i โŠข ( ( ๐‘˜ โˆˆ V โˆง ๐‘ง โˆˆ V ) โ†’ ( ๐‘€ +o ๐‘ง ) = ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) )
112 111 mpoeq3ia โŠข ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ๐‘€ +o ๐‘ง ) ) = ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) )
113 eqid โŠข โˆ… = โˆ…
114 seqomeq12 โŠข ( ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ๐‘€ +o ๐‘ง ) ) = ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) โˆง โˆ… = โˆ… ) โ†’ seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ๐‘€ +o ๐‘ง ) ) , โˆ… ) = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) )
115 112 113 114 mp2an โŠข seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ๐‘€ +o ๐‘ง ) ) , โˆ… ) = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… )
116 6 115 eqtri โŠข ๐ป = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… )
117 1 107 108 5 109 116 cantnfsuc โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ๐ผ โˆˆ ฯ‰ ) โ†’ ( ๐ป โ€˜ suc ๐ผ ) = ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) )
118 2 21 42 117 syl21anc โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ suc ๐ผ ) = ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) )
119 118 f1oeq2d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ๐ป โ€˜ suc ๐ผ ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) โ†” ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) +o ( ๐ป โ€˜ ๐ผ ) ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) ) )
120 106 119 mpbird โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ๐ป โ€˜ suc ๐ผ ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) )
121 sssucid โŠข dom ๐บ โŠ† suc dom ๐บ
122 121 10 sselid โŠข ( ๐œ‘ โ†’ ๐ผ โˆˆ suc dom ๐บ )
123 epelg โŠข ( ๐ผ โˆˆ dom ๐บ โ†’ ( ๐‘ฆ E ๐ผ โ†” ๐‘ฆ โˆˆ ๐ผ ) )
124 10 123 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ฆ E ๐ผ โ†” ๐‘ฆ โˆˆ ๐ผ ) )
125 124 biimpar โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ๐‘ฆ E ๐ผ )
126 ovexd โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โˆˆ V )
127 39 simpld โŠข ( ๐œ‘ โ†’ E We ( ๐น supp โˆ… ) )
128 5 oiiso โŠข ( ( ( ๐น supp โˆ… ) โˆˆ V โˆง E We ( ๐น supp โˆ… ) ) โ†’ ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โˆ… ) ) )
129 126 127 128 syl2anc โŠข ( ๐œ‘ โ†’ ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โˆ… ) ) )
130 129 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โˆ… ) ) )
131 5 oicl โŠข Ord dom ๐บ
132 ordelss โŠข ( ( Ord dom ๐บ โˆง ๐ผ โˆˆ dom ๐บ ) โ†’ ๐ผ โŠ† dom ๐บ )
133 131 10 132 sylancr โŠข ( ๐œ‘ โ†’ ๐ผ โŠ† dom ๐บ )
134 133 sselda โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ๐‘ฆ โˆˆ dom ๐บ )
135 10 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ๐ผ โˆˆ dom ๐บ )
136 isorel โŠข ( ( ๐บ Isom E , E ( dom ๐บ , ( ๐น supp โˆ… ) ) โˆง ( ๐‘ฆ โˆˆ dom ๐บ โˆง ๐ผ โˆˆ dom ๐บ ) ) โ†’ ( ๐‘ฆ E ๐ผ โ†” ( ๐บ โ€˜ ๐‘ฆ ) E ( ๐บ โ€˜ ๐ผ ) ) )
137 130 134 135 136 syl12anc โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ( ๐‘ฆ E ๐ผ โ†” ( ๐บ โ€˜ ๐‘ฆ ) E ( ๐บ โ€˜ ๐ผ ) ) )
138 125 137 mpbid โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ( ๐บ โ€˜ ๐‘ฆ ) E ( ๐บ โ€˜ ๐ผ ) )
139 fvex โŠข ( ๐บ โ€˜ ๐ผ ) โˆˆ V
140 139 epeli โŠข ( ( ๐บ โ€˜ ๐‘ฆ ) E ( ๐บ โ€˜ ๐ผ ) โ†” ( ๐บ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ โ€˜ ๐ผ ) )
141 138 140 sylib โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ๐ผ ) โ†’ ( ๐บ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ โ€˜ ๐ผ ) )
142 141 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ๐ผ ( ๐บ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ โ€˜ ๐ผ ) )
143 ffun โŠข ( ๐บ : dom ๐บ โŸถ ( ๐น supp โˆ… ) โ†’ Fun ๐บ )
144 26 143 ax-mp โŠข Fun ๐บ
145 funimass4 โŠข ( ( Fun ๐บ โˆง ๐ผ โŠ† dom ๐บ ) โ†’ ( ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) โ†” โˆ€ ๐‘ฆ โˆˆ ๐ผ ( ๐บ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ โ€˜ ๐ผ ) ) )
146 144 133 145 sylancr โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) โ†” โˆ€ ๐‘ฆ โˆˆ ๐ผ ( ๐บ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ โ€˜ ๐ผ ) ) )
147 142 146 mpbird โŠข ( ๐œ‘ โ†’ ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) )
148 13 a1i โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ฯ‰ โˆˆ On )
149 simpll โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ๐ด โˆˆ On )
150 simplr โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ๐น โˆˆ ๐‘† )
151 peano1 โŠข โˆ… โˆˆ ฯ‰
152 151 a1i โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ โˆ… โˆˆ ฯ‰ )
153 simpr1 โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ๐ผ โˆˆ suc dom ๐บ )
154 simpr2 โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ( ๐บ โ€˜ ๐ผ ) โˆˆ On )
155 simpr3 โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) )
156 1 148 149 5 150 116 152 153 154 155 cantnflt โŠข ( ( ( ๐ด โˆˆ On โˆง ๐น โˆˆ ๐‘† ) โˆง ( ๐ผ โˆˆ suc dom ๐บ โˆง ( ๐บ โ€˜ ๐ผ ) โˆˆ On โˆง ( ๐บ โ€œ ๐ผ ) โŠ† ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ( ๐ป โ€˜ ๐ผ ) โˆˆ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) )
157 2 21 122 31 147 156 syl23anc โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ ๐ผ ) โˆˆ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) )
158 24 ffnd โŠข ( ๐œ‘ โ†’ ๐น Fn ๐ด )
159 0ex โŠข โˆ… โˆˆ V
160 159 a1i โŠข ( ๐œ‘ โ†’ โˆ… โˆˆ V )
161 elsuppfn โŠข ( ( ๐น Fn ๐ด โˆง ๐ด โˆˆ On โˆง โˆ… โˆˆ V ) โ†’ ( ( ๐บ โ€˜ ๐ผ ) โˆˆ ( ๐น supp โˆ… ) โ†” ( ( ๐บ โ€˜ ๐ผ ) โˆˆ ๐ด โˆง ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… ) ) )
162 158 2 160 161 syl3anc โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€˜ ๐ผ ) โˆˆ ( ๐น supp โˆ… ) โ†” ( ( ๐บ โ€˜ ๐ผ ) โˆˆ ๐ด โˆง ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… ) ) )
163 simpr โŠข ( ( ( ๐บ โ€˜ ๐ผ ) โˆˆ ๐ด โˆง ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… ) โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… )
164 162 163 syl6bi โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€˜ ๐ผ ) โˆˆ ( ๐น supp โˆ… ) โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… ) )
165 28 164 mpd โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… )
166 on0eln0 โŠข ( ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On โ†’ ( โˆ… โˆˆ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ†” ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… ) )
167 36 166 syl โŠข ( ๐œ‘ โ†’ ( โˆ… โˆˆ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ†” ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โ‰  โˆ… ) )
168 165 167 mpbird โŠข ( ๐œ‘ โ†’ โˆ… โˆˆ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) )
169 omword1 โŠข ( ( ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On โˆง ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) โˆˆ On ) โˆง โˆ… โˆˆ ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โ†’ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โŠ† ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )
170 33 36 168 169 syl21anc โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โŠ† ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )
171 oaabs2 โŠข ( ( ( ( ๐ป โ€˜ ๐ผ ) โˆˆ ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โˆง ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) โˆˆ On ) โˆง ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) โŠ† ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) โ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )
172 157 38 170 171 syl21anc โŠข ( ๐œ‘ โ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) = ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )
173 172 f1oeq3d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ๐ป โ€˜ suc ๐ผ ) โ€“1-1-ontoโ†’ ( ( ๐ป โ€˜ ๐ผ ) +o ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) โ†” ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ๐ป โ€˜ suc ๐ผ ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) ) )
174 120 173 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ€˜ suc ๐ผ ) : ( ๐ป โ€˜ suc ๐ผ ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ( ๐บ โ€˜ ๐ผ ) ) ยทo ( ๐น โ€˜ ( ๐บ โ€˜ ๐ผ ) ) ) )