Metamath Proof Explorer

Theorem carsgclctunlem1

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 23-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
fiunelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fiunelcarsg.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
carsgclctunlem1.1 ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 𝑦 )
carsgclctunlem1.2 ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑂 )
Assertion carsgclctunlem1 ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) = Σ* 𝑦 ∈ 𝐴 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 fiunelcarsg.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
6 fiunelcarsg.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
7 carsgclctunlem1.1 ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 𝑦 )
8 carsgclctunlem1.2 ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑂 )
9 unieq ⊢ ( 𝑎 = ∅ → ∪ 𝑎 = ∪ ∅ )
10 9 ineq2d ⊢ ( 𝑎 = ∅ → ( 𝐸 ∩ ∪ 𝑎 ) = ( 𝐸 ∩ ∪ ∅ ) )
11 10 fveq2d ⊢ ( 𝑎 = ∅ → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ ∅ ) ) )
12 esumeq1 ⊢ ( 𝑎 = ∅ → Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = Σ* 𝑦 ∈ ∅ ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
13 11 12 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ↔ ( 𝑀 ‘ ( 𝐸 ∩ ∪ ∅ ) ) = Σ* 𝑦 ∈ ∅ ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
14 unieq ⊢ ( 𝑎 = 𝑏 → ∪ 𝑎 = ∪ 𝑏 )
15 14 ineq2d ⊢ ( 𝑎 = 𝑏 → ( 𝐸 ∩ ∪ 𝑎 ) = ( 𝐸 ∩ ∪ 𝑏 ) )
16 15 fveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) )
17 esumeq1 ⊢ ( 𝑎 = 𝑏 → Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
18 16 17 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ↔ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
19 unieq ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ∪ 𝑎 = ∪ ( 𝑏 ∪ { 𝑥 } ) )
20 19 ineq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ( 𝐸 ∩ ∪ 𝑎 ) = ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) )
21 20 fveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) )
22 esumeq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
23 21 22 eqeq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑥 } ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ↔ ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
24 unieq ⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴 )
25 24 ineq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐸 ∩ ∪ 𝑎 ) = ( 𝐸 ∩ ∪ 𝐴 ) )
26 25 fveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) )
27 esumeq1 ⊢ ( 𝑎 = 𝐴 → Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = Σ* 𝑦 ∈ 𝐴 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
28 26 27 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑎 ) ) = Σ* 𝑦 ∈ 𝑎 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ↔ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) = Σ* 𝑦 ∈ 𝐴 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
29 uni0 ⊢ ∪ ∅ = ∅
30 29 ineq2i ⊢ ( 𝐸 ∩ ∪ ∅ ) = ( 𝐸 ∩ ∅ )
31 in0 ⊢ ( 𝐸 ∩ ∅ ) = ∅
32 30 31 eqtri ⊢ ( 𝐸 ∩ ∪ ∅ ) = ∅
33 32 fveq2i ⊢ ( 𝑀 ‘ ( 𝐸 ∩ ∪ ∅ ) ) = ( 𝑀 ‘ ∅ )
34 esumnul ⊢ Σ* 𝑦 ∈ ∅ ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = 0
35 3 33 34 3eqtr4g ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ∅ ) ) = Σ* 𝑦 ∈ ∅ ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
36 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
37 36 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) )
38 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
39 38 ineq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 = 𝑥 ) → ( 𝐸 ∩ 𝑦 ) = ( 𝐸 ∩ 𝑥 ) )
40 39 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 = 𝑥 ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
41 simprr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) )
42 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
43 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝐸 ∈ 𝒫 𝑂 )
44 43 elpwincl1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ 𝑥 ) ∈ 𝒫 𝑂 )
45 42 44 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ∈ ( 0 [,] +∞ ) )
46 40 41 45 esumsn ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
48 37 47 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) +e Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) )
49 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) )
50 nfcv ⊢ Ⅎ 𝑦 𝑏
51 nfcv ⊢ Ⅎ 𝑦 { 𝑥 }
52 vex ⊢ 𝑏 ∈ V
53 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑏 ∈ V )
54 vsnex ⊢ { 𝑥 } ∈ V
55 54 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → { 𝑥 } ∈ V )
56 41 eldifbd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ¬ 𝑥 ∈ 𝑏 )
57 disjsn ⊢ ( ( 𝑏 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ 𝑏 )
58 56 57 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑏 ∩ { 𝑥 } ) = ∅ )
59 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
60 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ 𝑏 ) → 𝐸 ∈ 𝒫 𝑂 )
61 60 elpwincl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( 𝐸 ∩ 𝑦 ) ∈ 𝒫 𝑂 )
62 59 61 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ∈ ( 0 [,] +∞ ) )
63 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
64 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → 𝐸 ∈ 𝒫 𝑂 )
65 64 elpwincl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → ( 𝐸 ∩ 𝑦 ) ∈ 𝒫 𝑂 )
66 63 65 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ∈ ( 0 [,] +∞ ) )
67 49 50 51 53 55 58 62 66 esumsplit ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) +e Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) +e Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
69 uniun ⊢ ∪ ( 𝑏 ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ ∪ { 𝑥 } )
70 unisnv ⊢ ∪ { 𝑥 } = 𝑥
71 70 uneq2i ⊢ ( ∪ 𝑏 ∪ ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ 𝑥 )
72 69 71 eqtri ⊢ ∪ ( 𝑏 ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ 𝑥 )
73 72 ineq2i ⊢ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) )
74 73 fveq2i ⊢ ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) )
75 inass ⊢ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) = ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) )
76 indir ⊢ ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) = ( ( ∪ 𝑏 ∩ ∪ 𝑏 ) ∪ ( 𝑥 ∩ ∪ 𝑏 ) )
77 inidm ⊢ ( ∪ 𝑏 ∩ ∪ 𝑏 ) = ∪ 𝑏
78 77 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∪ 𝑏 ∩ ∪ 𝑏 ) = ∪ 𝑏 )
79 incom ⊢ ( ∪ 𝑏 ∩ 𝑥 ) = ( 𝑥 ∩ ∪ 𝑏 )
80 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Disj 𝑦 ∈ 𝐴 𝑦 )
81 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ⊆ 𝐴 )
82 81 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑏 ⊆ 𝐴 )
83 80 82 41 disjuniel ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∪ 𝑏 ∩ 𝑥 ) = ∅ )
84 79 83 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑥 ∩ ∪ 𝑏 ) = ∅ )
85 78 84 uneq12d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∩ ∪ 𝑏 ) ∪ ( 𝑥 ∩ ∪ 𝑏 ) ) = ( ∪ 𝑏 ∪ ∅ ) )
86 un0 ⊢ ( ∪ 𝑏 ∪ ∅ ) = ∪ 𝑏
87 85 86 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∩ ∪ 𝑏 ) ∪ ( 𝑥 ∩ ∪ 𝑏 ) ) = ∪ 𝑏 )
88 76 87 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) = ∪ 𝑏 )
89 88 ineq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) ) = ( 𝐸 ∩ ∪ 𝑏 ) )
90 75 89 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) = ( 𝐸 ∩ ∪ 𝑏 ) )
91 90 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) )
92 indif2 ⊢ ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) ) = ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 )
93 uncom ⊢ ( ∪ 𝑏 ∪ 𝑥 ) = ( 𝑥 ∪ ∪ 𝑏 )
94 93 difeq1i ⊢ ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) = ( ( 𝑥 ∪ ∪ 𝑏 ) ∖ ∪ 𝑏 )
95 difun2 ⊢ ( ( 𝑥 ∪ ∪ 𝑏 ) ∖ ∪ 𝑏 ) = ( 𝑥 ∖ ∪ 𝑏 )
96 disj3 ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ ↔ 𝑥 = ( 𝑥 ∖ ∪ 𝑏 ) )
97 96 biimpi ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ → 𝑥 = ( 𝑥 ∖ ∪ 𝑏 ) )
98 95 97 eqtr4id ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ → ( ( 𝑥 ∪ ∪ 𝑏 ) ∖ ∪ 𝑏 ) = 𝑥 )
99 94 98 eqtrid ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ → ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) = 𝑥 )
100 84 99 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) = 𝑥 )
101 100 ineq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) ) = ( 𝐸 ∩ 𝑥 ) )
102 92 101 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) = ( 𝐸 ∩ 𝑥 ) )
103 102 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
104 91 103 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) )
105 1 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑂 ∈ 𝑉 )
106 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
107 3 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( 𝑀 ‘ ∅ ) = 0 )
108 4 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
109 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ∈ Fin )
110 5 109 sylan ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ∈ Fin )
111 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
112 81 111 sstrd ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ⊆ ( toCaraSiga ‘ 𝑀 ) )
113 105 106 107 108 110 112 fiunelcarsg ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) )
114 1 2 elcarsg ⊢ ( 𝜑 → ( ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∪ 𝑏 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∪ 𝑏 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
116 113 115 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( ∪ 𝑏 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
117 116 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
118 117 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
119 43 elpwincl1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∈ 𝒫 𝑂 )
120 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) )
121 120 ineq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑒 ∩ ∪ 𝑏 ) = ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) )
122 121 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) )
123 120 difeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑒 ∖ ∪ 𝑏 ) = ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) )
124 123 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) )
125 122 124 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) )
126 120 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑀 ‘ 𝑒 ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
127 125 126 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) ) )
128 119 127 rspcdv ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) → ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) ) )
129 118 128 mpd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
130 104 129 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
131 130 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
132 74 131 eqtr4id ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +e ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) )
133 48 68 132 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
134 133 ex ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
135 13 18 23 28 35 134 5 findcard2d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) = Σ* 𝑦 ∈ 𝐴 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )