Metamath Proof Explorer


Theorem ackbij1lem12

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

Ref Expression
Hypothesis ackbij.f F=x𝒫ωFincardyxy×𝒫y
Assertion ackbij1lem12 B𝒫ωFinABFAFB

Proof

Step Hyp Ref Expression
1 ackbij.f F=x𝒫ωFincardyxy×𝒫y
2 1 ackbij1lem10 F:𝒫ωFinω
3 1 ackbij1lem11 B𝒫ωFinABA𝒫ωFin
4 ffvelcdm F:𝒫ωFinωA𝒫ωFinFAω
5 2 3 4 sylancr B𝒫ωFinABFAω
6 difssd B𝒫ωFinABBAB
7 1 ackbij1lem11 B𝒫ωFinBABBA𝒫ωFin
8 6 7 syldan B𝒫ωFinABBA𝒫ωFin
9 ffvelcdm F:𝒫ωFinωBA𝒫ωFinFBAω
10 2 8 9 sylancr B𝒫ωFinABFBAω
11 nnaword1 FAωFBAωFAFA+𝑜FBA
12 5 10 11 syl2anc B𝒫ωFinABFAFA+𝑜FBA
13 disjdif ABA=
14 13 a1i B𝒫ωFinABABA=
15 1 ackbij1lem9 A𝒫ωFinBA𝒫ωFinABA=FABA=FA+𝑜FBA
16 3 8 14 15 syl3anc B𝒫ωFinABFABA=FA+𝑜FBA
17 undif ABABA=B
18 17 biimpi ABABA=B
19 18 adantl B𝒫ωFinABABA=B
20 19 fveq2d B𝒫ωFinABFABA=FB
21 16 20 eqtr3d B𝒫ωFinABFA+𝑜FBA=FB
22 12 21 sseqtrd B𝒫ωFinABFAFB