# Metamath Proof Explorer

## Theorem cantnflem1c

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

Ref Expression
Hypotheses cantnfs.s 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ( 𝜑𝐴 ∈ On )
cantnfs.b ( 𝜑𝐵 ∈ On )
oemapval.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
oemapval.f ( 𝜑𝐹𝑆 )
oemapval.g ( 𝜑𝐺𝑆 )
oemapvali.r ( 𝜑𝐹 𝑇 𝐺 )
oemapvali.x 𝑋 = { 𝑐𝐵 ∣ ( 𝐹𝑐 ) ∈ ( 𝐺𝑐 ) }
cantnflem1.o 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
Assertion cantnflem1c ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝐺 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 cantnflem1.o 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
10 3 ad3antrrr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝐵 ∈ On )
11 simplr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑥𝐵 )
12 1 2 3 cantnfs ( 𝜑 → ( 𝐺𝑆 ↔ ( 𝐺 : 𝐵𝐴𝐺 finSupp ∅ ) ) )
13 6 12 mpbid ( 𝜑 → ( 𝐺 : 𝐵𝐴𝐺 finSupp ∅ ) )
14 13 simpld ( 𝜑𝐺 : 𝐵𝐴 )
15 14 ffnd ( 𝜑𝐺 Fn 𝐵 )
16 15 ad3antrrr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝐺 Fn 𝐵 )
17 1 2 3 4 5 6 7 8 9 cantnflem1b ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) → 𝑋 ⊆ ( 𝑂𝑢 ) )
18 17 ad2antrr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑋 ⊆ ( 𝑂𝑢 ) )
19 simprr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ( 𝑂𝑢 ) ∈ 𝑥 )
20 1 2 3 4 5 6 7 8 oemapvali ( 𝜑 → ( 𝑋𝐵 ∧ ( 𝐹𝑋 ) ∈ ( 𝐺𝑋 ) ∧ ∀ 𝑤𝐵 ( 𝑋𝑤 → ( 𝐹𝑤 ) = ( 𝐺𝑤 ) ) ) )
21 20 simp1d ( 𝜑𝑋𝐵 )
22 onelon ( ( 𝐵 ∈ On ∧ 𝑋𝐵 ) → 𝑋 ∈ On )
23 3 21 22 syl2anc ( 𝜑𝑋 ∈ On )
24 23 ad3antrrr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑋 ∈ On )
25 onss ( 𝐵 ∈ On → 𝐵 ⊆ On )
26 3 25 syl ( 𝜑𝐵 ⊆ On )
27 26 sselda ( ( 𝜑𝑥𝐵 ) → 𝑥 ∈ On )
28 27 ad4ant13 ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ On )
29 ontr2 ( ( 𝑋 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑋 ⊆ ( 𝑂𝑢 ) ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) → 𝑋𝑥 ) )
30 24 28 29 syl2anc ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ( ( 𝑋 ⊆ ( 𝑂𝑢 ) ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) → 𝑋𝑥 ) )
31 18 19 30 mp2and ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑋𝑥 )
32 eleq2w ( 𝑤 = 𝑥 → ( 𝑋𝑤𝑋𝑥 ) )
33 fveq2 ( 𝑤 = 𝑥 → ( 𝐹𝑤 ) = ( 𝐹𝑥 ) )
34 fveq2 ( 𝑤 = 𝑥 → ( 𝐺𝑤 ) = ( 𝐺𝑥 ) )
35 33 34 eqeq12d ( 𝑤 = 𝑥 → ( ( 𝐹𝑤 ) = ( 𝐺𝑤 ) ↔ ( 𝐹𝑥 ) = ( 𝐺𝑥 ) ) )
36 32 35 imbi12d ( 𝑤 = 𝑥 → ( ( 𝑋𝑤 → ( 𝐹𝑤 ) = ( 𝐺𝑤 ) ) ↔ ( 𝑋𝑥 → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) ) ) )
37 20 simp3d ( 𝜑 → ∀ 𝑤𝐵 ( 𝑋𝑤 → ( 𝐹𝑤 ) = ( 𝐺𝑤 ) ) )
38 37 ad3antrrr ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ∀ 𝑤𝐵 ( 𝑋𝑤 → ( 𝐹𝑤 ) = ( 𝐺𝑤 ) ) )
39 36 38 11 rspcdva ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ( 𝑋𝑥 → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) ) )
40 31 39 mpd ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ( 𝐹𝑥 ) = ( 𝐺𝑥 ) )
41 simprl ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ( 𝐹𝑥 ) ≠ ∅ )
42 40 41 eqnetrrd ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → ( 𝐺𝑥 ) ≠ ∅ )
43 fvn0elsupp ( ( ( 𝐵 ∈ On ∧ 𝑥𝐵 ) ∧ ( 𝐺 Fn 𝐵 ∧ ( 𝐺𝑥 ) ≠ ∅ ) ) → 𝑥 ∈ ( 𝐺 supp ∅ ) )
44 10 11 16 42 43 syl22anc ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( 𝑂𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥𝐵 ) ∧ ( ( 𝐹𝑥 ) ≠ ∅ ∧ ( 𝑂𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝐺 supp ∅ ) )