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 𝑆 = 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 ∅ ) )