This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackbij1lem16

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypothesis ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
Assertion ackbij1lem16 
|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` A ) = ( F ` B ) -> A = B ) )

Proof

Step Hyp Ref Expression
1 ackbij.f 
 |-  F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
2 inss1 
 |-  ( ~P _om i^i Fin ) C_ ~P _om
3 2 sseli 
 |-  ( A e. ( ~P _om i^i Fin ) -> A e. ~P _om )
4 3 elpwid 
 |-  ( A e. ( ~P _om i^i Fin ) -> A C_ _om )
5 4 adantr 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> A C_ _om )
6 2 sseli 
 |-  ( B e. ( ~P _om i^i Fin ) -> B e. ~P _om )
7 6 elpwid 
 |-  ( B e. ( ~P _om i^i Fin ) -> B C_ _om )
8 7 adantl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> B C_ _om )
9 5 8 unssd 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) C_ _om )
10 inss2 
 |-  ( ~P _om i^i Fin ) C_ Fin
11 10 sseli 
 |-  ( A e. ( ~P _om i^i Fin ) -> A e. Fin )
12 10 sseli 
 |-  ( B e. ( ~P _om i^i Fin ) -> B e. Fin )
13 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
14 11 12 13 syl2an 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) e. Fin )
15 nnunifi 
 |-  ( ( ( A u. B ) C_ _om /\ ( A u. B ) e. Fin ) -> U. ( A u. B ) e. _om )
16 9 14 15 syl2anc 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> U. ( A u. B ) e. _om )
17 peano2 
 |-  ( U. ( A u. B ) e. _om -> suc U. ( A u. B ) e. _om )
18 16 17 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> suc U. ( A u. B ) e. _om )
19 ineq2 
 |-  ( a = (/) -> ( A i^i a ) = ( A i^i (/) ) )
20 19 fveq2d 
 |-  ( a = (/) -> ( F ` ( A i^i a ) ) = ( F ` ( A i^i (/) ) ) )
21 ineq2 
 |-  ( a = (/) -> ( B i^i a ) = ( B i^i (/) ) )
22 21 fveq2d 
 |-  ( a = (/) -> ( F ` ( B i^i a ) ) = ( F ` ( B i^i (/) ) ) )
23 20 22 eqeq12d 
 |-  ( a = (/) -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) <-> ( F ` ( A i^i (/) ) ) = ( F ` ( B i^i (/) ) ) ) )
24 19 21 eqeq12d 
 |-  ( a = (/) -> ( ( A i^i a ) = ( B i^i a ) <-> ( A i^i (/) ) = ( B i^i (/) ) ) )
25 23 24 imbi12d 
 |-  ( a = (/) -> ( ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) <-> ( ( F ` ( A i^i (/) ) ) = ( F ` ( B i^i (/) ) ) -> ( A i^i (/) ) = ( B i^i (/) ) ) ) )
26 25 imbi2d 
 |-  ( a = (/) -> ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) ) <-> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i (/) ) ) = ( F ` ( B i^i (/) ) ) -> ( A i^i (/) ) = ( B i^i (/) ) ) ) ) )
27 ineq2 
 |-  ( a = b -> ( A i^i a ) = ( A i^i b ) )
28 27 fveq2d 
 |-  ( a = b -> ( F ` ( A i^i a ) ) = ( F ` ( A i^i b ) ) )
29 ineq2 
 |-  ( a = b -> ( B i^i a ) = ( B i^i b ) )
30 29 fveq2d 
 |-  ( a = b -> ( F ` ( B i^i a ) ) = ( F ` ( B i^i b ) ) )
31 28 30 eqeq12d 
 |-  ( a = b -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) <-> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
32 27 29 eqeq12d 
 |-  ( a = b -> ( ( A i^i a ) = ( B i^i a ) <-> ( A i^i b ) = ( B i^i b ) ) )
33 31 32 imbi12d 
 |-  ( a = b -> ( ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) <-> ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) ) )
34 33 imbi2d 
 |-  ( a = b -> ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) ) <-> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) ) ) )
35 ineq2 
 |-  ( a = suc b -> ( A i^i a ) = ( A i^i suc b ) )
36 35 fveq2d 
 |-  ( a = suc b -> ( F ` ( A i^i a ) ) = ( F ` ( A i^i suc b ) ) )
37 ineq2 
 |-  ( a = suc b -> ( B i^i a ) = ( B i^i suc b ) )
38 37 fveq2d 
 |-  ( a = suc b -> ( F ` ( B i^i a ) ) = ( F ` ( B i^i suc b ) ) )
39 36 38 eqeq12d 
 |-  ( a = suc b -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) <-> ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) )
40 35 37 eqeq12d 
 |-  ( a = suc b -> ( ( A i^i a ) = ( B i^i a ) <-> ( A i^i suc b ) = ( B i^i suc b ) ) )
41 39 40 imbi12d 
 |-  ( a = suc b -> ( ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) <-> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) )
42 41 imbi2d 
 |-  ( a = suc b -> ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) ) <-> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
43 ineq2 
 |-  ( a = suc U. ( A u. B ) -> ( A i^i a ) = ( A i^i suc U. ( A u. B ) ) )
44 43 fveq2d 
 |-  ( a = suc U. ( A u. B ) -> ( F ` ( A i^i a ) ) = ( F ` ( A i^i suc U. ( A u. B ) ) ) )
45 ineq2 
 |-  ( a = suc U. ( A u. B ) -> ( B i^i a ) = ( B i^i suc U. ( A u. B ) ) )
46 45 fveq2d 
 |-  ( a = suc U. ( A u. B ) -> ( F ` ( B i^i a ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) )
47 44 46 eqeq12d 
 |-  ( a = suc U. ( A u. B ) -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) <-> ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) ) )
48 43 45 eqeq12d 
 |-  ( a = suc U. ( A u. B ) -> ( ( A i^i a ) = ( B i^i a ) <-> ( A i^i suc U. ( A u. B ) ) = ( B i^i suc U. ( A u. B ) ) ) )
49 47 48 imbi12d 
 |-  ( a = suc U. ( A u. B ) -> ( ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) <-> ( ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) -> ( A i^i suc U. ( A u. B ) ) = ( B i^i suc U. ( A u. B ) ) ) ) )
50 49 imbi2d 
 |-  ( a = suc U. ( A u. B ) -> ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i a ) ) = ( F ` ( B i^i a ) ) -> ( A i^i a ) = ( B i^i a ) ) ) <-> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) -> ( A i^i suc U. ( A u. B ) ) = ( B i^i suc U. ( A u. B ) ) ) ) ) )
51 in0 
 |-  ( A i^i (/) ) = (/)
52 in0 
 |-  ( B i^i (/) ) = (/)
53 51 52 eqtr4i 
 |-  ( A i^i (/) ) = ( B i^i (/) )
54 53 2a1i 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i (/) ) ) = ( F ` ( B i^i (/) ) ) -> ( A i^i (/) ) = ( B i^i (/) ) ) )
55 simp13 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) )
56 3simpa 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) )
57 ackbij1lem2 
 |-  ( b e. A -> ( A i^i suc b ) = ( { b } u. ( A i^i b ) ) )
58 57 fveq2d 
 |-  ( b e. A -> ( F ` ( A i^i suc b ) ) = ( F ` ( { b } u. ( A i^i b ) ) ) )
59 58 3ad2ant2 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( A i^i suc b ) ) = ( F ` ( { b } u. ( A i^i b ) ) ) )
60 ackbij1lem4 
 |-  ( b e. _om -> { b } e. ( ~P _om i^i Fin ) )
61 60 adantr 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> { b } e. ( ~P _om i^i Fin ) )
62 simprl 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> A e. ( ~P _om i^i Fin ) )
63 inss1 
 |-  ( A i^i b ) C_ A
64 1 ackbij1lem11 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ ( A i^i b ) C_ A ) -> ( A i^i b ) e. ( ~P _om i^i Fin ) )
65 62 63 64 sylancl 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( A i^i b ) e. ( ~P _om i^i Fin ) )
66 incom 
 |-  ( { b } i^i ( A i^i b ) ) = ( ( A i^i b ) i^i { b } )
67 inss2 
 |-  ( A i^i b ) C_ b
68 nnord 
 |-  ( b e. _om -> Ord b )
69 orddisj 
 |-  ( Ord b -> ( b i^i { b } ) = (/) )
70 68 69 syl 
 |-  ( b e. _om -> ( b i^i { b } ) = (/) )
71 70 adantr 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( b i^i { b } ) = (/) )
72 ssdisj 
 |-  ( ( ( A i^i b ) C_ b /\ ( b i^i { b } ) = (/) ) -> ( ( A i^i b ) i^i { b } ) = (/) )
73 67 71 72 sylancr 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( ( A i^i b ) i^i { b } ) = (/) )
74 66 73 eqtrid 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( { b } i^i ( A i^i b ) ) = (/) )
75 1 ackbij1lem9 
 |-  ( ( { b } e. ( ~P _om i^i Fin ) /\ ( A i^i b ) e. ( ~P _om i^i Fin ) /\ ( { b } i^i ( A i^i b ) ) = (/) ) -> ( F ` ( { b } u. ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) )
76 61 65 74 75 syl3anc 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( F ` ( { b } u. ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) )
77 76 3ad2ant1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( { b } u. ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) )
78 59 77 eqtrd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( A i^i suc b ) ) = ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) )
79 56 78 syl3an1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( A i^i suc b ) ) = ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) )
80 ackbij1lem2 
 |-  ( b e. B -> ( B i^i suc b ) = ( { b } u. ( B i^i b ) ) )
81 80 fveq2d 
 |-  ( b e. B -> ( F ` ( B i^i suc b ) ) = ( F ` ( { b } u. ( B i^i b ) ) ) )
82 81 3ad2ant3 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( B i^i suc b ) ) = ( F ` ( { b } u. ( B i^i b ) ) ) )
83 simprr 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> B e. ( ~P _om i^i Fin ) )
84 inss1 
 |-  ( B i^i b ) C_ B
85 1 ackbij1lem11 
 |-  ( ( B e. ( ~P _om i^i Fin ) /\ ( B i^i b ) C_ B ) -> ( B i^i b ) e. ( ~P _om i^i Fin ) )
86 83 84 85 sylancl 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( B i^i b ) e. ( ~P _om i^i Fin ) )
87 incom 
 |-  ( { b } i^i ( B i^i b ) ) = ( ( B i^i b ) i^i { b } )
88 inss2 
 |-  ( B i^i b ) C_ b
89 ssdisj 
 |-  ( ( ( B i^i b ) C_ b /\ ( b i^i { b } ) = (/) ) -> ( ( B i^i b ) i^i { b } ) = (/) )
90 88 71 89 sylancr 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( ( B i^i b ) i^i { b } ) = (/) )
91 87 90 eqtrid 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( { b } i^i ( B i^i b ) ) = (/) )
92 1 ackbij1lem9 
 |-  ( ( { b } e. ( ~P _om i^i Fin ) /\ ( B i^i b ) e. ( ~P _om i^i Fin ) /\ ( { b } i^i ( B i^i b ) ) = (/) ) -> ( F ` ( { b } u. ( B i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) )
93 61 86 91 92 syl3anc 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( F ` ( { b } u. ( B i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) )
94 93 3ad2ant1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( { b } u. ( B i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) )
95 82 94 eqtrd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( B i^i suc b ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) )
96 56 95 syl3an1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( B i^i suc b ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) )
97 55 79 96 3eqtr3d 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) )
98 1 ackbij1lem10 
 |-  F : ( ~P _om i^i Fin ) --> _om
99 98 ffvelcdmi 
 |-  ( { b } e. ( ~P _om i^i Fin ) -> ( F ` { b } ) e. _om )
100 61 99 syl 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( F ` { b } ) e. _om )
101 98 ffvelcdmi 
 |-  ( ( A i^i b ) e. ( ~P _om i^i Fin ) -> ( F ` ( A i^i b ) ) e. _om )
102 65 101 syl 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( F ` ( A i^i b ) ) e. _om )
103 98 ffvelcdmi 
 |-  ( ( B i^i b ) e. ( ~P _om i^i Fin ) -> ( F ` ( B i^i b ) ) e. _om )
104 86 103 syl 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( F ` ( B i^i b ) ) e. _om )
105 nnacan 
 |-  ( ( ( F ` { b } ) e. _om /\ ( F ` ( A i^i b ) ) e. _om /\ ( F ` ( B i^i b ) ) e. _om ) -> ( ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) <-> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
106 100 102 104 105 syl3anc 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) ) -> ( ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) <-> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
107 106 3adant3 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) <-> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
108 107 3ad2ant1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( ( ( F ` { b } ) +o ( F ` ( A i^i b ) ) ) = ( ( F ` { b } ) +o ( F ` ( B i^i b ) ) ) <-> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
109 97 108 mpbid 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) )
110 uneq2 
 |-  ( ( A i^i b ) = ( B i^i b ) -> ( { b } u. ( A i^i b ) ) = ( { b } u. ( B i^i b ) ) )
111 110 adantl 
 |-  ( ( ( b e. A /\ b e. B ) /\ ( A i^i b ) = ( B i^i b ) ) -> ( { b } u. ( A i^i b ) ) = ( { b } u. ( B i^i b ) ) )
112 57 ad2antrr 
 |-  ( ( ( b e. A /\ b e. B ) /\ ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( { b } u. ( A i^i b ) ) )
113 80 ad2antlr 
 |-  ( ( ( b e. A /\ b e. B ) /\ ( A i^i b ) = ( B i^i b ) ) -> ( B i^i suc b ) = ( { b } u. ( B i^i b ) ) )
114 111 112 113 3eqtr4d 
 |-  ( ( ( b e. A /\ b e. B ) /\ ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) )
115 114 ex 
 |-  ( ( b e. A /\ b e. B ) -> ( ( A i^i b ) = ( B i^i b ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
116 115 3adant1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( ( A i^i b ) = ( B i^i b ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
117 109 116 embantd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ b e. B ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
118 117 3exp 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( b e. A -> ( b e. B -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
119 simp13 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) )
120 119 eqcomd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> ( F ` ( B i^i suc b ) ) = ( F ` ( A i^i suc b ) ) )
121 simp12r 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> B e. ( ~P _om i^i Fin ) )
122 simp12l 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> A e. ( ~P _om i^i Fin ) )
123 simp11 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> b e. _om )
124 simp3 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> b e. B )
125 simp2 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> -. b e. A )
126 1 ackbij1lem15 
 |-  ( ( ( B e. ( ~P _om i^i Fin ) /\ A e. ( ~P _om i^i Fin ) ) /\ ( b e. _om /\ b e. B /\ -. b e. A ) ) -> -. ( F ` ( B i^i suc b ) ) = ( F ` ( A i^i suc b ) ) )
127 121 122 123 124 125 126 syl23anc 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> -. ( F ` ( B i^i suc b ) ) = ( F ` ( A i^i suc b ) ) )
128 120 127 pm2.21dd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ b e. B ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
129 128 3exp 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( -. b e. A -> ( b e. B -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
130 118 129 pm2.61d 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( b e. B -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) )
131 simp13 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) )
132 simp12l 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> A e. ( ~P _om i^i Fin ) )
133 simp12r 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> B e. ( ~P _om i^i Fin ) )
134 simp11 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> b e. _om )
135 simp2 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> b e. A )
136 simp3 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> -. b e. B )
137 1 ackbij1lem15 
 |-  ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( b e. _om /\ b e. A /\ -. b e. B ) ) -> -. ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) )
138 132 133 134 135 136 137 syl23anc 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> -. ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) )
139 131 138 pm2.21dd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ b e. A /\ -. b e. B ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
140 139 3exp 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( b e. A -> ( -. b e. B -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
141 simp13 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ -. b e. B ) -> ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) )
142 ackbij1lem1 
 |-  ( -. b e. A -> ( A i^i suc b ) = ( A i^i b ) )
143 142 adantr 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( A i^i suc b ) = ( A i^i b ) )
144 143 fveq2d 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( F ` ( A i^i suc b ) ) = ( F ` ( A i^i b ) ) )
145 ackbij1lem1 
 |-  ( -. b e. B -> ( B i^i suc b ) = ( B i^i b ) )
146 145 adantl 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( B i^i suc b ) = ( B i^i b ) )
147 146 fveq2d 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( F ` ( B i^i suc b ) ) = ( F ` ( B i^i b ) ) )
148 144 147 eqeq12d 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) <-> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
149 148 biimpd 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
150 149 3adant1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ -. b e. B ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) ) )
151 141 150 mpd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ -. b e. B ) -> ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) )
152 143 146 eqeq12d 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( ( A i^i suc b ) = ( B i^i suc b ) <-> ( A i^i b ) = ( B i^i b ) ) )
153 152 biimprd 
 |-  ( ( -. b e. A /\ -. b e. B ) -> ( ( A i^i b ) = ( B i^i b ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
154 153 3adant1 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ -. b e. B ) -> ( ( A i^i b ) = ( B i^i b ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
155 151 154 embantd 
 |-  ( ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) /\ -. b e. A /\ -. b e. B ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
156 155 3exp 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( -. b e. A -> ( -. b e. B -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
157 140 156 pm2.61d 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( -. b e. B -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) )
158 130 157 pm2.61d 
 |-  ( ( b e. _om /\ ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) /\ ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) )
159 158 3exp 
 |-  ( b e. _om -> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
160 159 com34 
 |-  ( b e. _om -> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
161 160 a2d 
 |-  ( b e. _om -> ( ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i b ) ) = ( F ` ( B i^i b ) ) -> ( A i^i b ) = ( B i^i b ) ) ) -> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc b ) ) = ( F ` ( B i^i suc b ) ) -> ( A i^i suc b ) = ( B i^i suc b ) ) ) ) )
162 26 34 42 50 54 161 finds 
 |-  ( suc U. ( A u. B ) e. _om -> ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) -> ( A i^i suc U. ( A u. B ) ) = ( B i^i suc U. ( A u. B ) ) ) ) )
163 18 162 mpcom 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) -> ( A i^i suc U. ( A u. B ) ) = ( B i^i suc U. ( A u. B ) ) ) )
164 omsson 
 |-  _om C_ On
165 9 164 sstrdi 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) C_ On )
166 onsucuni 
 |-  ( ( A u. B ) C_ On -> ( A u. B ) C_ suc U. ( A u. B ) )
167 165 166 syl 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) C_ suc U. ( A u. B ) )
168 167 unssad 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> A C_ suc U. ( A u. B ) )
169 dfss2 
 |-  ( A C_ suc U. ( A u. B ) <-> ( A i^i suc U. ( A u. B ) ) = A )
170 168 169 sylib 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A i^i suc U. ( A u. B ) ) = A )
171 170 fveq2d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` A ) )
172 167 unssbd 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> B C_ suc U. ( A u. B ) )
173 dfss2 
 |-  ( B C_ suc U. ( A u. B ) <-> ( B i^i suc U. ( A u. B ) ) = B )
174 172 173 sylib 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( B i^i suc U. ( A u. B ) ) = B )
175 174 fveq2d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( F ` ( B i^i suc U. ( A u. B ) ) ) = ( F ` B ) )
176 171 175 eqeq12d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` ( A i^i suc U. ( A u. B ) ) ) = ( F ` ( B i^i suc U. ( A u. B ) ) ) <-> ( F ` A ) = ( F ` B ) ) )
177 170 174 eqeq12d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( A i^i suc U. ( A u. B ) ) = ( B i^i suc U. ( A u. B ) ) <-> A = B ) )
178 163 176 177 3imtr3d 
 |-  ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( ( F ` A ) = ( F ` B ) -> A = B ) )