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

Metamath Proof Explorer

Theorem cantnflem1a

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
oemapval.f ⊢ φ → F ∈ S
oemapval.g ⊢ φ → G ∈ S
oemapvali.r ⊢ φ → F T G
oemapvali.x ⊢ X = ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c
Assertion cantnflem1a ⊢ φ → X ∈ supp ∅⁡ G

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 oemapval.f ⊢ φ → F ∈ S
6 oemapval.g ⊢ φ → G ∈ S
7 oemapvali.r ⊢ φ → F T G
8 oemapvali.x ⊢ X = ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c
9 1 2 3 4 5 6 7 8 oemapvali ⊢ φ → X ∈ B ∧ F ⁡ X ∈ G ⁡ X ∧ ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w
10 9 simp1d ⊢ φ → X ∈ B
11 9 simp2d ⊢ φ → F ⁡ X ∈ G ⁡ X
12 11 ne0d ⊢ φ → G ⁡ X ≠ ∅
13 1 2 3 cantnfs ⊢ φ → G ∈ S ↔ G : B ⟶ A ∧ finSupp ∅⁡ G
14 6 13 mpbid ⊢ φ → G : B ⟶ A ∧ finSupp ∅⁡ G
15 14 simpld ⊢ φ → G : B ⟶ A
16 15 ffnd ⊢ φ → G Fn B
17 0ex ⊢ ∅ ∈ V
18 17 a1i ⊢ φ → ∅ ∈ V
19 elsuppfn ⊢ G Fn B ∧ B ∈ On ∧ ∅ ∈ V → X ∈ supp ∅⁡ G ↔ X ∈ B ∧ G ⁡ X ≠ ∅
20 16 3 18 19 syl3anc ⊢ φ → X ∈ supp ∅⁡ G ↔ X ∈ B ∧ G ⁡ X ≠ ∅
21 10 12 20 mpbir2and ⊢ φ → X ∈ supp ∅⁡ G