Metamath Proof Explorer

Theorem cardiun

Description: The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003)

Ref Expression
Assertion cardiun ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 → ( card ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵 ) )

Proof

Step Hyp Ref Expression
1 abrexexg ⊢ ( 𝐴 ∈ 𝑉 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ∈ V )
2 vex ⊢ 𝑦 ∈ V
3 eqeq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = ( card ‘ 𝐵 ) ↔ 𝑦 = ( card ‘ 𝐵 ) ) )
4 3 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( card ‘ 𝐵 ) ) )
5 2 4 elab ⊢ ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( card ‘ 𝐵 ) )
6 cardidm ⊢ ( card ‘ ( card ‘ 𝐵 ) ) = ( card ‘ 𝐵 )
7 fveq2 ⊢ ( 𝑦 = ( card ‘ 𝐵 ) → ( card ‘ 𝑦 ) = ( card ‘ ( card ‘ 𝐵 ) ) )
8 id ⊢ ( 𝑦 = ( card ‘ 𝐵 ) → 𝑦 = ( card ‘ 𝐵 ) )
9 6 7 8 3eqtr4a ⊢ ( 𝑦 = ( card ‘ 𝐵 ) → ( card ‘ 𝑦 ) = 𝑦 )
10 9 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( card ‘ 𝐵 ) → ( card ‘ 𝑦 ) = 𝑦 )
11 5 10 sylbi ⊢ ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } → ( card ‘ 𝑦 ) = 𝑦 )
12 11 rgen ⊢ ∀ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ( card ‘ 𝑦 ) = 𝑦
13 carduni ⊢ ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ∈ V → ( ∀ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ( card ‘ 𝑦 ) = 𝑦 → ( card ‘ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ) )
14 1 12 13 mpisyl ⊢ ( 𝐴 ∈ 𝑉 → ( card ‘ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } )
15 fvex ⊢ ( card ‘ 𝐵 ) ∈ V
16 15 dfiun2 ⊢ ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) }
17 16 fveq2i ⊢ ( card ‘ ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) ) = ( card ‘ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( card ‘ 𝐵 ) } )
18 14 17 16 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ( card ‘ ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) ) = ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) )
19 18 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 ) → ( card ‘ ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) ) = ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) )
20 iuneq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 → ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
21 20 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
22 21 fveq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 ) → ( card ‘ ∪ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) ) = ( card ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
23 19 22 21 3eqtr3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 ) → ( card ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
24 23 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( card ‘ 𝐵 ) = 𝐵 → ( card ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵 ) )