ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ennnfonelemg GIF version

Theorem ennnfonelemg 12406
Description: Lemma for ennnfone 12428. Closure for 𝐺. (Contributed by Jim Kingdon, 20-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
ennnfonelemh.f (𝜑𝐹:ω–onto𝐴)
ennnfonelemh.ne (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
ennnfonelemh.g 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
ennnfonelemh.n 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
ennnfonelemh.j 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
ennnfonelemh.h 𝐻 = seq0(𝐺, 𝐽)
Assertion
Ref Expression
ennnfonelemg ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝑓𝐺𝑗) ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
Distinct variable groups:   𝐴,𝑔,𝑥,𝑦   𝑔,𝐹,𝑥,𝑦   𝑥,𝑁   𝑓,𝑔,𝑥,𝑦   𝑔,𝑗,𝑥,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑓,𝑔,𝑗,𝑘,𝑛)   𝐴(𝑓,𝑗,𝑘,𝑛)   𝐹(𝑓,𝑗,𝑘,𝑛)   𝐺(𝑥,𝑦,𝑓,𝑔,𝑗,𝑘,𝑛)   𝐻(𝑥,𝑦,𝑓,𝑔,𝑗,𝑘,𝑛)   𝐽(𝑥,𝑦,𝑓,𝑔,𝑗,𝑘,𝑛)   𝑁(𝑦,𝑓,𝑔,𝑗,𝑘,𝑛)

Proof of Theorem ennnfonelemg
StepHypRef Expression
1 ennnfonelemh.g . . . 4 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
21a1i 9 . . 3 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩}))))
3 simpr 110 . . . . . . 7 ((𝑥 = 𝑓𝑦 = 𝑗) → 𝑦 = 𝑗)
43fveq2d 5521 . . . . . 6 ((𝑥 = 𝑓𝑦 = 𝑗) → (𝐹𝑦) = (𝐹𝑗))
53imaeq2d 4972 . . . . . 6 ((𝑥 = 𝑓𝑦 = 𝑗) → (𝐹𝑦) = (𝐹𝑗))
64, 5eleq12d 2248 . . . . 5 ((𝑥 = 𝑓𝑦 = 𝑗) → ((𝐹𝑦) ∈ (𝐹𝑦) ↔ (𝐹𝑗) ∈ (𝐹𝑗)))
7 simpl 109 . . . . 5 ((𝑥 = 𝑓𝑦 = 𝑗) → 𝑥 = 𝑓)
87dmeqd 4831 . . . . . . . 8 ((𝑥 = 𝑓𝑦 = 𝑗) → dom 𝑥 = dom 𝑓)
98, 4opeq12d 3788 . . . . . . 7 ((𝑥 = 𝑓𝑦 = 𝑗) → ⟨dom 𝑥, (𝐹𝑦)⟩ = ⟨dom 𝑓, (𝐹𝑗)⟩)
109sneqd 3607 . . . . . 6 ((𝑥 = 𝑓𝑦 = 𝑗) → {⟨dom 𝑥, (𝐹𝑦)⟩} = {⟨dom 𝑓, (𝐹𝑗)⟩})
117, 10uneq12d 3292 . . . . 5 ((𝑥 = 𝑓𝑦 = 𝑗) → (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩}) = (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}))
126, 7, 11ifbieq12d 3562 . . . 4 ((𝑥 = 𝑓𝑦 = 𝑗) → if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})) = if((𝐹𝑗) ∈ (𝐹𝑗), 𝑓, (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩})))
1312adantl 277 . . 3 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ (𝑥 = 𝑓𝑦 = 𝑗)) → if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})) = if((𝐹𝑗) ∈ (𝐹𝑗), 𝑓, (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩})))
14 ssrab2 3242 . . . 4 {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ⊆ (𝐴pm ω)
15 simprl 529 . . . 4 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → 𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
1614, 15sselid 3155 . . 3 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → 𝑓 ∈ (𝐴pm ω))
17 simprr 531 . . 3 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → 𝑗 ∈ ω)
18 simplrl 535 . . . 4 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ (𝐹𝑗) ∈ (𝐹𝑗)) → 𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
19 dmeq 4829 . . . . . 6 (𝑔 = (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) → dom 𝑔 = dom (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}))
2019eleq1d 2246 . . . . 5 (𝑔 = (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) → (dom 𝑔 ∈ ω ↔ dom (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) ∈ ω))
21 omex 4594 . . . . . . . 8 ω ∈ V
22 ennnfonelemh.f . . . . . . . 8 (𝜑𝐹:ω–onto𝐴)
23 focdmex 6118 . . . . . . . 8 (ω ∈ V → (𝐹:ω–onto𝐴𝐴 ∈ V))
2421, 22, 23mpsyl 65 . . . . . . 7 (𝜑𝐴 ∈ V)
2524ad2antrr 488 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → 𝐴 ∈ V)
2621a1i 9 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → ω ∈ V)
27 simplrl 535 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → 𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
28 elrabi 2892 . . . . . . . . . 10 (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} → 𝑓 ∈ (𝐴pm ω))
29 elpmi 6669 . . . . . . . . . 10 (𝑓 ∈ (𝐴pm ω) → (𝑓:dom 𝑓𝐴 ∧ dom 𝑓 ⊆ ω))
3028, 29syl 14 . . . . . . . . 9 (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} → (𝑓:dom 𝑓𝐴 ∧ dom 𝑓 ⊆ ω))
3130simpld 112 . . . . . . . 8 (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} → 𝑓:dom 𝑓𝐴)
3227, 31syl 14 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → 𝑓:dom 𝑓𝐴)
33 dmeq 4829 . . . . . . . . . . 11 (𝑔 = 𝑓 → dom 𝑔 = dom 𝑓)
3433eleq1d 2246 . . . . . . . . . 10 (𝑔 = 𝑓 → (dom 𝑔 ∈ ω ↔ dom 𝑓 ∈ ω))
3534elrab 2895 . . . . . . . . 9 (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ↔ (𝑓 ∈ (𝐴pm ω) ∧ dom 𝑓 ∈ ω))
3635simprbi 275 . . . . . . . 8 (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} → dom 𝑓 ∈ ω)
3727, 36syl 14 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → dom 𝑓 ∈ ω)
38 nnord 4613 . . . . . . . . 9 (dom 𝑓 ∈ ω → Ord dom 𝑓)
3937, 38syl 14 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → Ord dom 𝑓)
40 ordirr 4543 . . . . . . . 8 (Ord dom 𝑓 → ¬ dom 𝑓 ∈ dom 𝑓)
4139, 40syl 14 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → ¬ dom 𝑓 ∈ dom 𝑓)
4222adantr 276 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → 𝐹:ω–onto𝐴)
43 fof 5440 . . . . . . . . . 10 (𝐹:ω–onto𝐴𝐹:ω⟶𝐴)
4442, 43syl 14 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → 𝐹:ω⟶𝐴)
4544, 17ffvelcdmd 5654 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝐹𝑗) ∈ 𝐴)
4645adantr 276 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → (𝐹𝑗) ∈ 𝐴)
47 fsnunf 5718 . . . . . . 7 ((𝑓:dom 𝑓𝐴 ∧ (dom 𝑓 ∈ ω ∧ ¬ dom 𝑓 ∈ dom 𝑓) ∧ (𝐹𝑗) ∈ 𝐴) → (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}):(dom 𝑓 ∪ {dom 𝑓})⟶𝐴)
4832, 37, 41, 46, 47syl121anc 1243 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}):(dom 𝑓 ∪ {dom 𝑓})⟶𝐴)
49 df-suc 4373 . . . . . . . . 9 suc dom 𝑓 = (dom 𝑓 ∪ {dom 𝑓})
50 peano2 4596 . . . . . . . . 9 (dom 𝑓 ∈ ω → suc dom 𝑓 ∈ ω)
5149, 50eqeltrrid 2265 . . . . . . . 8 (dom 𝑓 ∈ ω → (dom 𝑓 ∪ {dom 𝑓}) ∈ ω)
5237, 51syl 14 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → (dom 𝑓 ∪ {dom 𝑓}) ∈ ω)
53 elomssom 4606 . . . . . . 7 ((dom 𝑓 ∪ {dom 𝑓}) ∈ ω → (dom 𝑓 ∪ {dom 𝑓}) ⊆ ω)
5452, 53syl 14 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → (dom 𝑓 ∪ {dom 𝑓}) ⊆ ω)
55 elpm2r 6668 . . . . . 6 (((𝐴 ∈ V ∧ ω ∈ V) ∧ ((𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}):(dom 𝑓 ∪ {dom 𝑓})⟶𝐴 ∧ (dom 𝑓 ∪ {dom 𝑓}) ⊆ ω)) → (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) ∈ (𝐴pm ω))
5625, 26, 48, 54, 55syl22anc 1239 . . . . 5 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) ∈ (𝐴pm ω))
5748fdmd 5374 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → dom (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) = (dom 𝑓 ∪ {dom 𝑓}))
5857, 52eqeltrd 2254 . . . . 5 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → dom (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) ∈ ω)
5920, 56, 58elrabd 2897 . . . 4 (((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) ∧ ¬ (𝐹𝑗) ∈ (𝐹𝑗)) → (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩}) ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
60 ennnfonelemh.dceq . . . . . 6 (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
6160adantr 276 . . . . 5 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
6261, 42, 17ennnfonelemdc 12402 . . . 4 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → DECID (𝐹𝑗) ∈ (𝐹𝑗))
6318, 59, 62ifcldadc 3565 . . 3 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → if((𝐹𝑗) ∈ (𝐹𝑗), 𝑓, (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩})) ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
642, 13, 16, 17, 63ovmpod 6004 . 2 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝑓𝐺𝑗) = if((𝐹𝑗) ∈ (𝐹𝑗), 𝑓, (𝑓 ∪ {⟨dom 𝑓, (𝐹𝑗)⟩})))
6564, 63eqeltrd 2254 1 ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝑓𝐺𝑗) ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  DECID wdc 834   = wceq 1353  wcel 2148  wne 2347  wral 2455  wrex 2456  {crab 2459  Vcvv 2739  cun 3129  wss 3131  c0 3424  ifcif 3536  {csn 3594  cop 3597  cmpt 4066  Ord word 4364  suc csuc 4367  ωcom 4591  ccnv 4627  dom cdm 4628  cima 4631  wf 5214  ontowfo 5216  cfv 5218  (class class class)co 5877  cmpo 5879  freccfrec 6393  pm cpm 6651  0cc0 7813  1c1 7814   + caddc 7816  cmin 8130  0cn0 9178  cz 9255  seqcseq 10447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pm 6653
This theorem is referenced by:  ennnfonelemh  12407  ennnfonelem0  12408  ennnfonelemp1  12409  ennnfonelemom  12411
  Copyright terms: Public domain W3C validator