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

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