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 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ∈ ( 0 [,] +∞ ) )
46 40 41 45 esumsn ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
48 37 47 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) +𝑒 Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) )
49 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) )
50 nfcv ⊢ Ⅎ 𝑦 𝑏
51 nfcv ⊢ Ⅎ 𝑦 { 𝑥 }
52 vex ⊢ 𝑏 ∈ V
53 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑏 ∈ V )
54 snex ⊢ { 𝑥 } ∈ 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ 𝑏 ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ∈ ( 0 [,] +∞ ) )
63 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
64 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → 𝐸 ∈ 𝒫 𝑂 )
65 64 elpwincl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → ( 𝐸 ∩ 𝑦 ) ∈ 𝒫 𝑂 )
66 63 65 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑦 ∈ { 𝑥 } ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ∈ ( 0 [,] +∞ ) )
67 49 50 51 53 55 58 62 66 esumsplit ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) +𝑒 Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) +𝑒 Σ* 𝑦 ∈ { 𝑥 } ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
69 uniun ⊢ ∪ ( 𝑏 ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ ∪ { 𝑥 } )
70 vex ⊢ 𝑥 ∈ V
71 70 unisn ⊢ ∪ { 𝑥 } = 𝑥
72 71 uneq2i ⊢ ( ∪ 𝑏 ∪ ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ 𝑥 )
73 69 72 eqtri ⊢ ∪ ( 𝑏 ∪ { 𝑥 } ) = ( ∪ 𝑏 ∪ 𝑥 )
74 73 ineq2i ⊢ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) )
75 74 fveq2i ⊢ ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) )
76 inass ⊢ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) = ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) )
77 indir ⊢ ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) = ( ( ∪ 𝑏 ∩ ∪ 𝑏 ) ∪ ( 𝑥 ∩ ∪ 𝑏 ) )
78 inidm ⊢ ( ∪ 𝑏 ∩ ∪ 𝑏 ) = ∪ 𝑏
79 78 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∪ 𝑏 ∩ ∪ 𝑏 ) = ∪ 𝑏 )
80 incom ⊢ ( ∪ 𝑏 ∩ 𝑥 ) = ( 𝑥 ∩ ∪ 𝑏 )
81 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Disj 𝑦 ∈ 𝐴 𝑦 )
82 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ⊆ 𝐴 )
83 82 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑏 ⊆ 𝐴 )
84 81 83 41 disjuniel ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∪ 𝑏 ∩ 𝑥 ) = ∅ )
85 80 84 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑥 ∩ ∪ 𝑏 ) = ∅ )
86 79 85 uneq12d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∩ ∪ 𝑏 ) ∪ ( 𝑥 ∩ ∪ 𝑏 ) ) = ( ∪ 𝑏 ∪ ∅ ) )
87 un0 ⊢ ( ∪ 𝑏 ∪ ∅ ) = ∪ 𝑏
88 86 87 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∩ ∪ 𝑏 ) ∪ ( 𝑥 ∩ ∪ 𝑏 ) ) = ∪ 𝑏 )
89 77 88 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) = ∪ 𝑏 )
90 89 ineq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∩ ∪ 𝑏 ) ) = ( 𝐸 ∩ ∪ 𝑏 ) )
91 76 90 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) = ( 𝐸 ∩ ∪ 𝑏 ) )
92 91 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) )
93 indif2 ⊢ ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) ) = ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 )
94 uncom ⊢ ( ∪ 𝑏 ∪ 𝑥 ) = ( 𝑥 ∪ ∪ 𝑏 )
95 94 difeq1i ⊢ ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) = ( ( 𝑥 ∪ ∪ 𝑏 ) ∖ ∪ 𝑏 )
96 difun2 ⊢ ( ( 𝑥 ∪ ∪ 𝑏 ) ∖ ∪ 𝑏 ) = ( 𝑥 ∖ ∪ 𝑏 )
97 disj3 ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ ↔ 𝑥 = ( 𝑥 ∖ ∪ 𝑏 ) )
98 97 biimpi ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ → 𝑥 = ( 𝑥 ∖ ∪ 𝑏 ) )
99 96 98 eqtr4id ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ → ( ( 𝑥 ∪ ∪ 𝑏 ) ∖ ∪ 𝑏 ) = 𝑥 )
100 95 99 syl5eq ⊢ ( ( 𝑥 ∩ ∪ 𝑏 ) = ∅ → ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) = 𝑥 )
101 85 100 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) = 𝑥 )
102 101 ineq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ ( ( ∪ 𝑏 ∪ 𝑥 ) ∖ ∪ 𝑏 ) ) = ( 𝐸 ∩ 𝑥 ) )
103 93 102 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) = ( 𝐸 ∩ 𝑥 ) )
104 103 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) )
105 92 104 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) )
106 1 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑂 ∈ 𝑉 )
107 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
108 3 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( 𝑀 ‘ ∅ ) = 0 )
109 4 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
110 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ∈ Fin )
111 5 110 sylan ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ∈ Fin )
112 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
113 82 112 sstrd ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → 𝑏 ⊆ ( toCaraSiga ‘ 𝑀 ) )
114 106 107 108 109 111 113 fiunelcarsg ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) )
115 1 2 elcarsg ⊢ ( 𝜑 → ( ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∪ 𝑏 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( ∪ 𝑏 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∪ 𝑏 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
117 114 116 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ( ∪ 𝑏 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
118 117 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
119 118 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
120 43 elpwincl1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∈ 𝒫 𝑂 )
121 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) )
122 121 ineq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑒 ∩ ∪ 𝑏 ) = ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) )
123 122 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) )
124 121 difeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑒 ∖ ∪ 𝑏 ) = ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) )
125 124 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) = ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) )
126 123 125 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) )
127 121 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( 𝑀 ‘ 𝑒 ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
128 126 127 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑒 = ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) ) )
129 120 128 rspcdv ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ 𝑒 ) → ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) ) )
130 119 129 mpd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ∖ ∪ 𝑏 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
131 105 130 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ( ∪ 𝑏 ∪ 𝑥 ) ) ) )
133 75 132 eqtr4id ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∩ 𝑥 ) ) ) )
134 48 68 133 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
135 134 ex ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑏 ) ) = Σ* 𝑦 ∈ 𝑏 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ( 𝑏 ∪ { 𝑥 } ) ) ) = Σ* 𝑦 ∈ ( 𝑏 ∪ { 𝑥 } ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) ) )
136 13 18 23 28 35 135 5 findcard2d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) = Σ* 𝑦 ∈ 𝐴 ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )