cantnflem1a

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

	Ref	Expression
Hypotheses	cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	oemapval.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
	oemapval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
	oemapval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
	oemapvali.r	⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
	oemapvali.x	⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
Assertion	cantnflem1a	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 supp ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		oemapval.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5		oemapval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6		oemapval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
7		oemapvali.r	⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
8		oemapvali.x	⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
9	1 2 3 4 5 6 7 8	oemapvali	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
10	9	simp1d	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11	9	simp2d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) )
12	11	ne0d	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ ∅ )
13	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
14	6 13	mpbid	⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
15	14	simpld	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
16	15	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
17		0ex	⊢ ∅ ∈ V
18	17	a1i	⊢ ( 𝜑 → ∅ ∈ V )
19		elsuppfn	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
20	16 3 18 19	syl3anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
21	10 12 20	mpbir2and	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 supp ∅ ) )

Metamath Proof Explorer

Theorem cantnflem1a

Proof