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

Metamath Proof Explorer

Theorem ackbij1lem9

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

Ref Expression
Hypothesis ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion ackbij1lem9 ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2 elinel2 ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ Fin )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ Fin )
4 snfi ⊢ { 𝑦 } ∈ Fin
5 elinel1 ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ 𝒫 ω )
6 5 elpwid ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ⊆ ω )
7 6 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ⊆ ω )
8 onfin2 ⊢ ω = ( On ∩ Fin )
9 inss2 ⊢ ( On ∩ Fin ) ⊆ Fin
10 8 9 eqsstri ⊢ ω ⊆ Fin
11 7 10 sstrdi ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ⊆ Fin )
12 11 sselda ⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ Fin )
13 pwfi ⊢ ( 𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin )
14 12 13 sylib ⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐴 ) → 𝒫 𝑦 ∈ Fin )
15 xpfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ 𝒫 𝑦 ∈ Fin ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
16 4 14 15 sylancr ⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐴 ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
17 16 ralrimiva ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∀ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
18 iunfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
19 3 17 18 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
20 ficardid ⊢ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) )
21 19 20 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) )
22 elinel2 ⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ∈ Fin )
23 22 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ∈ Fin )
24 elinel1 ⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ∈ 𝒫 ω )
25 24 elpwid ⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → 𝐵 ⊆ ω )
26 25 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ ω )
27 26 10 sstrdi ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ Fin )
28 27 sselda ⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ Fin )
29 28 13 sylib ⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝒫 𝑦 ∈ Fin )
30 4 29 15 sylancr ⊢ ( ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
31 30 ralrimiva ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∀ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
32 iunfi ⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
33 23 31 32 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
34 ficardid ⊢ ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) )
35 33 34 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) )
36 djuen ⊢ ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∧ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) )
37 21 35 36 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) )
38 djudisj ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) = ∅ )
39 38 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) = ∅ )
40 endjudisj ⊢ ( ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ∧ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ∧ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∩ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∪ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) )
41 19 33 39 40 syl3anc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∪ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) )
42 iunxun ⊢ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) = ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∪ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) )
43 41 42 breqtrrdi ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) )
44 entr ⊢ ( ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∧ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ⊔ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) )
45 37 43 44 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) )
46 carden2b ⊢ ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ≈ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) )
47 45 46 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) )
48 ficardom ⊢ ( ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω )
49 19 48 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω )
50 ficardom ⊢ ( ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω )
51 33 50 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω )
52 nnadju ⊢ ( ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ∧ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) )
53 49 51 52 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) ⊔ ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) )
54 47 53 eqtr3d ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) )
55 ackbij1lem6 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) )
56 55 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) )
57 1 ackbij1lem7 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) )
58 56 57 syl ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( card ‘ ∪ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( { 𝑦 } × 𝒫 𝑦 ) ) )
59 1 ackbij1lem7 ⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ 𝐴 ) = ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) )
60 1 ackbij1lem7 ⊢ ( 𝐵 ∈ ( 𝒫 ω ∩ Fin ) → ( 𝐹 ‘ 𝐵 ) = ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) )
61 59 60 oveqan12d ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) → ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) )
62 61 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) = ( ( card ‘ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝒫 𝑦 ) ) +o ( card ‘ ∪ 𝑦 ∈ 𝐵 ( { 𝑦 } × 𝒫 𝑦 ) ) ) )
63 54 58 62 3eqtr4d ⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐹 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) +o ( 𝐹 ‘ 𝐵 ) ) )