Metamath Proof Explorer


Theorem ficardunOLD

Description: Obsolete version of ficardun as of 3-Jul-2024. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Mario Carneiro, 28-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ficardunOLD ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( card ‘ ( 𝐴𝐵 ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 finnum ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
2 finnum ( 𝐵 ∈ Fin → 𝐵 ∈ dom card )
3 cardadju ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
4 1 2 3 syl2an ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
5 4 3adant3 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( 𝐴𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
6 5 ensymd ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴𝐵 ) )
7 endjudisj ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( 𝐴𝐵 ) ≈ ( 𝐴𝐵 ) )
8 entr ( ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴𝐵 ) ∧ ( 𝐴𝐵 ) ≈ ( 𝐴𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴𝐵 ) )
9 6 7 8 syl2anc ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴𝐵 ) )
10 carden2b ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴𝐵 ) → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( card ‘ ( 𝐴𝐵 ) ) )
11 9 10 syl ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( card ‘ ( 𝐴𝐵 ) ) )
12 ficardom ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
13 ficardom ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
14 nnacl ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ ω )
15 cardnn ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ ω → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
16 14 15 syl ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
17 12 13 16 syl2an ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
18 17 3adant3 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
19 11 18 eqtr3d ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴𝐵 ) = ∅ ) → ( card ‘ ( 𝐴𝐵 ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )