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

Theorem difinfsnlem 6994
 Description: Lemma for difinfsn 6995. The case where we need to swap 𝐵 and (inr‘∅) in building the mapping 𝐺. (Contributed by Jim Kingdon, 9-Aug-2023.)
Hypotheses
Ref Expression
difinfsnlem.dc (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
difinfsnlem.b (𝜑𝐵𝐴)
difinfsnlem.f (𝜑𝐹:(ω ⊔ 1o)–1-1𝐴)
difinfsnlem.fb (𝜑 → (𝐹‘(inr‘∅)) ≠ 𝐵)
difinfsnlem.g 𝐺 = (𝑛 ∈ ω ↦ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))))
Assertion
Ref Expression
difinfsnlem (𝜑𝐺:ω–1-1→(𝐴 ∖ {𝐵}))
Distinct variable groups:   𝐴,𝑛,𝑥,𝑦   𝐵,𝑛,𝑥,𝑦   𝑛,𝐹,𝑥,𝑦   𝜑,𝑛
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐺(𝑥,𝑦,𝑛)

Proof of Theorem difinfsnlem
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 difinfsnlem.f . . . . . . . 8 (𝜑𝐹:(ω ⊔ 1o)–1-1𝐴)
2 f1f 5337 . . . . . . . 8 (𝐹:(ω ⊔ 1o)–1-1𝐴𝐹:(ω ⊔ 1o)⟶𝐴)
31, 2syl 14 . . . . . . 7 (𝜑𝐹:(ω ⊔ 1o)⟶𝐴)
4 0lt1o 6346 . . . . . . . 8 ∅ ∈ 1o
5 djurcl 6947 . . . . . . . 8 (∅ ∈ 1o → (inr‘∅) ∈ (ω ⊔ 1o))
64, 5mp1i 10 . . . . . . 7 (𝜑 → (inr‘∅) ∈ (ω ⊔ 1o))
73, 6ffvelrnd 5565 . . . . . 6 (𝜑 → (𝐹‘(inr‘∅)) ∈ 𝐴)
8 difinfsnlem.fb . . . . . . 7 (𝜑 → (𝐹‘(inr‘∅)) ≠ 𝐵)
9 elsni 3551 . . . . . . . 8 ((𝐹‘(inr‘∅)) ∈ {𝐵} → (𝐹‘(inr‘∅)) = 𝐵)
109necon3ai 2358 . . . . . . 7 ((𝐹‘(inr‘∅)) ≠ 𝐵 → ¬ (𝐹‘(inr‘∅)) ∈ {𝐵})
118, 10syl 14 . . . . . 6 (𝜑 → ¬ (𝐹‘(inr‘∅)) ∈ {𝐵})
127, 11eldifd 3087 . . . . 5 (𝜑 → (𝐹‘(inr‘∅)) ∈ (𝐴 ∖ {𝐵}))
1312ad2antrr 480 . . . 4 (((𝜑𝑛 ∈ ω) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) → (𝐹‘(inr‘∅)) ∈ (𝐴 ∖ {𝐵}))
143adantr 274 . . . . . . 7 ((𝜑𝑛 ∈ ω) → 𝐹:(ω ⊔ 1o)⟶𝐴)
15 djulcl 6946 . . . . . . . 8 (𝑛 ∈ ω → (inl‘𝑛) ∈ (ω ⊔ 1o))
1615adantl 275 . . . . . . 7 ((𝜑𝑛 ∈ ω) → (inl‘𝑛) ∈ (ω ⊔ 1o))
1714, 16ffvelrnd 5565 . . . . . 6 ((𝜑𝑛 ∈ ω) → (𝐹‘(inl‘𝑛)) ∈ 𝐴)
1817adantr 274 . . . . 5 (((𝜑𝑛 ∈ ω) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) → (𝐹‘(inl‘𝑛)) ∈ 𝐴)
19 elsni 3551 . . . . . . 7 ((𝐹‘(inl‘𝑛)) ∈ {𝐵} → (𝐹‘(inl‘𝑛)) = 𝐵)
2019con3i 622 . . . . . 6 (¬ (𝐹‘(inl‘𝑛)) = 𝐵 → ¬ (𝐹‘(inl‘𝑛)) ∈ {𝐵})
2120adantl 275 . . . . 5 (((𝜑𝑛 ∈ ω) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) → ¬ (𝐹‘(inl‘𝑛)) ∈ {𝐵})
2218, 21eldifd 3087 . . . 4 (((𝜑𝑛 ∈ ω) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) → (𝐹‘(inl‘𝑛)) ∈ (𝐴 ∖ {𝐵}))
23 difinfsnlem.dc . . . . . 6 (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
2423adantr 274 . . . . 5 ((𝜑𝑛 ∈ ω) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
25 difinfsnlem.b . . . . . . 7 (𝜑𝐵𝐴)
2625adantr 274 . . . . . 6 ((𝜑𝑛 ∈ ω) → 𝐵𝐴)
27 eqeq12 2153 . . . . . . . 8 ((𝑥 = (𝐹‘(inl‘𝑛)) ∧ 𝑦 = 𝐵) → (𝑥 = 𝑦 ↔ (𝐹‘(inl‘𝑛)) = 𝐵))
2827dcbid 824 . . . . . . 7 ((𝑥 = (𝐹‘(inl‘𝑛)) ∧ 𝑦 = 𝐵) → (DECID 𝑥 = 𝑦DECID (𝐹‘(inl‘𝑛)) = 𝐵))
2928rspc2gv 2806 . . . . . 6 (((𝐹‘(inl‘𝑛)) ∈ 𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID (𝐹‘(inl‘𝑛)) = 𝐵))
3017, 26, 29syl2anc 409 . . . . 5 ((𝜑𝑛 ∈ ω) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID (𝐹‘(inl‘𝑛)) = 𝐵))
3124, 30mpd 13 . . . 4 ((𝜑𝑛 ∈ ω) → DECID (𝐹‘(inl‘𝑛)) = 𝐵)
3213, 22, 31ifcldadc 3507 . . 3 ((𝜑𝑛 ∈ ω) → if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) ∈ (𝐴 ∖ {𝐵}))
3332ralrimiva 2509 . 2 (𝜑 → ∀𝑛 ∈ ω if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) ∈ (𝐴 ∖ {𝐵}))
34 simplr 520 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (𝐹‘(inl‘𝑛)) = 𝐵)
35 simpr 109 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (𝐹‘(inl‘𝑚)) = 𝐵)
3634, 35eqtr4d 2176 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (𝐹‘(inl‘𝑛)) = (𝐹‘(inl‘𝑚)))
371ad3antrrr 484 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝐹:(ω ⊔ 1o)–1-1𝐴)
3815ad2antrl 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → (inl‘𝑛) ∈ (ω ⊔ 1o))
3938ad2antrr 480 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑛) ∈ (ω ⊔ 1o))
40 simprr 522 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → 𝑚 ∈ ω)
4140ad2antrr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝑚 ∈ ω)
42 djulcl 6946 . . . . . . . . . 10 (𝑚 ∈ ω → (inl‘𝑚) ∈ (ω ⊔ 1o))
4341, 42syl 14 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑚) ∈ (ω ⊔ 1o))
44 f1veqaeq 5679 . . . . . . . . 9 ((𝐹:(ω ⊔ 1o)–1-1𝐴 ∧ ((inl‘𝑛) ∈ (ω ⊔ 1o) ∧ (inl‘𝑚) ∈ (ω ⊔ 1o))) → ((𝐹‘(inl‘𝑛)) = (𝐹‘(inl‘𝑚)) → (inl‘𝑛) = (inl‘𝑚)))
4537, 39, 43, 44syl12anc 1215 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ((𝐹‘(inl‘𝑛)) = (𝐹‘(inl‘𝑚)) → (inl‘𝑛) = (inl‘𝑚)))
4636, 45mpd 13 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑛) = (inl‘𝑚))
47 inl11 6960 . . . . . . . 8 ((𝑛 ∈ ω ∧ 𝑚 ∈ ω) → ((inl‘𝑛) = (inl‘𝑚) ↔ 𝑛 = 𝑚))
4847ad3antlr 485 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ((inl‘𝑛) = (inl‘𝑚) ↔ 𝑛 = 𝑚))
4946, 48mpbid 146 . . . . . 6 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝑛 = 𝑚)
5049a1d 22 . . . . 5 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
5140ad2antrr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝑚 ∈ ω)
52 djune 6973 . . . . . . . . . . 11 ((𝑚 ∈ ω ∧ ∅ ∈ 1o) → (inl‘𝑚) ≠ (inr‘∅))
5352necomd 2395 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ ∅ ∈ 1o) → (inr‘∅) ≠ (inl‘𝑚))
5451, 4, 53sylancl 410 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (inr‘∅) ≠ (inl‘𝑚))
5554neneqd 2330 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (inr‘∅) = (inl‘𝑚))
561ad3antrrr 484 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝐹:(ω ⊔ 1o)–1-1𝐴)
574, 5mp1i 10 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (inr‘∅) ∈ (ω ⊔ 1o))
5840, 42syl 14 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → (inl‘𝑚) ∈ (ω ⊔ 1o))
5958ad2antrr 480 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑚) ∈ (ω ⊔ 1o))
60 f1veqaeq 5679 . . . . . . . . 9 ((𝐹:(ω ⊔ 1o)–1-1𝐴 ∧ ((inr‘∅) ∈ (ω ⊔ 1o) ∧ (inl‘𝑚) ∈ (ω ⊔ 1o))) → ((𝐹‘(inr‘∅)) = (𝐹‘(inl‘𝑚)) → (inr‘∅) = (inl‘𝑚)))
6156, 57, 59, 60syl12anc 1215 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ((𝐹‘(inr‘∅)) = (𝐹‘(inl‘𝑚)) → (inr‘∅) = (inl‘𝑚)))
6255, 61mtod 653 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (𝐹‘(inr‘∅)) = (𝐹‘(inl‘𝑚)))
63 simplr 520 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (𝐹‘(inl‘𝑛)) = 𝐵)
6463iftrued 3487 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = (𝐹‘(inr‘∅)))
65 simpr 109 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (𝐹‘(inl‘𝑚)) = 𝐵)
6665iffalsed 3490 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) = (𝐹‘(inl‘𝑚)))
6764, 66eqeq12d 2155 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) ↔ (𝐹‘(inr‘∅)) = (𝐹‘(inl‘𝑚))))
6862, 67mtbird 663 . . . . . 6 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))))
6968pm2.21d 609 . . . . 5 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
7023adantr 274 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
713adantr 274 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → 𝐹:(ω ⊔ 1o)⟶𝐴)
7271, 58ffvelrnd 5565 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → (𝐹‘(inl‘𝑚)) ∈ 𝐴)
7325adantr 274 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → 𝐵𝐴)
74 eqeq12 2153 . . . . . . . . . . 11 ((𝑥 = (𝐹‘(inl‘𝑚)) ∧ 𝑦 = 𝐵) → (𝑥 = 𝑦 ↔ (𝐹‘(inl‘𝑚)) = 𝐵))
7574dcbid 824 . . . . . . . . . 10 ((𝑥 = (𝐹‘(inl‘𝑚)) ∧ 𝑦 = 𝐵) → (DECID 𝑥 = 𝑦DECID (𝐹‘(inl‘𝑚)) = 𝐵))
7675rspc2gv 2806 . . . . . . . . 9 (((𝐹‘(inl‘𝑚)) ∈ 𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID (𝐹‘(inl‘𝑚)) = 𝐵))
7772, 73, 76syl2anc 409 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦DECID (𝐹‘(inl‘𝑚)) = 𝐵))
7870, 77mpd 13 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → DECID (𝐹‘(inl‘𝑚)) = 𝐵)
79 exmiddc 822 . . . . . . 7 (DECID (𝐹‘(inl‘𝑚)) = 𝐵 → ((𝐹‘(inl‘𝑚)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑚)) = 𝐵))
8078, 79syl 14 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → ((𝐹‘(inl‘𝑚)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑚)) = 𝐵))
8180adantr 274 . . . . 5 (((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) → ((𝐹‘(inl‘𝑚)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑚)) = 𝐵))
8250, 69, 81mpjaodan 788 . . . 4 (((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ (𝐹‘(inl‘𝑛)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
83 simprl 521 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → 𝑛 ∈ ω)
8483ad2antrr 480 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝑛 ∈ ω)
85 djune 6973 . . . . . . . . . 10 ((𝑛 ∈ ω ∧ ∅ ∈ 1o) → (inl‘𝑛) ≠ (inr‘∅))
8684, 4, 85sylancl 410 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑛) ≠ (inr‘∅))
8786neneqd 2330 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (inl‘𝑛) = (inr‘∅))
881ad3antrrr 484 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝐹:(ω ⊔ 1o)–1-1𝐴)
8938ad2antrr 480 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑛) ∈ (ω ⊔ 1o))
904, 5mp1i 10 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (inr‘∅) ∈ (ω ⊔ 1o))
91 f1veqaeq 5679 . . . . . . . . 9 ((𝐹:(ω ⊔ 1o)–1-1𝐴 ∧ ((inl‘𝑛) ∈ (ω ⊔ 1o) ∧ (inr‘∅) ∈ (ω ⊔ 1o))) → ((𝐹‘(inl‘𝑛)) = (𝐹‘(inr‘∅)) → (inl‘𝑛) = (inr‘∅)))
9288, 89, 90, 91syl12anc 1215 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ((𝐹‘(inl‘𝑛)) = (𝐹‘(inr‘∅)) → (inl‘𝑛) = (inr‘∅)))
9387, 92mtod 653 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (𝐹‘(inl‘𝑛)) = (𝐹‘(inr‘∅)))
94 simplr 520 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (𝐹‘(inl‘𝑛)) = 𝐵)
9594iffalsed 3490 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = (𝐹‘(inl‘𝑛)))
96 simpr 109 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (𝐹‘(inl‘𝑚)) = 𝐵)
9796iftrued 3487 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) = (𝐹‘(inr‘∅)))
9895, 97eqeq12d 2155 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) ↔ (𝐹‘(inl‘𝑛)) = (𝐹‘(inr‘∅))))
9993, 98mtbird 663 . . . . . 6 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))))
10099pm2.21d 609 . . . . 5 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
101 simplr 520 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (𝐹‘(inl‘𝑛)) = 𝐵)
102101iffalsed 3490 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = (𝐹‘(inl‘𝑛)))
103 simpr 109 . . . . . . . . 9 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ¬ (𝐹‘(inl‘𝑚)) = 𝐵)
104103iffalsed 3490 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) = (𝐹‘(inl‘𝑚)))
105102, 104eqeq12d 2155 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) ↔ (𝐹‘(inl‘𝑛)) = (𝐹‘(inl‘𝑚))))
1061ad3antrrr 484 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → 𝐹:(ω ⊔ 1o)–1-1𝐴)
10738ad2antrr 480 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑛) ∈ (ω ⊔ 1o))
10858ad2antrr 480 . . . . . . . 8 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (inl‘𝑚) ∈ (ω ⊔ 1o))
109106, 107, 108, 44syl12anc 1215 . . . . . . 7 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ((𝐹‘(inl‘𝑛)) = (𝐹‘(inl‘𝑚)) → (inl‘𝑛) = (inl‘𝑚)))
110105, 109sylbid 149 . . . . . 6 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → (inl‘𝑛) = (inl‘𝑚)))
11147ad3antlr 485 . . . . . 6 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → ((inl‘𝑛) = (inl‘𝑚) ↔ 𝑛 = 𝑚))
112110, 111sylibd 148 . . . . 5 ((((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) ∧ ¬ (𝐹‘(inl‘𝑚)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
11380adantr 274 . . . . 5 (((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) → ((𝐹‘(inl‘𝑚)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑚)) = 𝐵))
114100, 112, 113mpjaodan 788 . . . 4 (((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) ∧ ¬ (𝐹‘(inl‘𝑛)) = 𝐵) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
115 exmiddc 822 . . . . . 6 (DECID (𝐹‘(inl‘𝑛)) = 𝐵 → ((𝐹‘(inl‘𝑛)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑛)) = 𝐵))
11631, 115syl 14 . . . . 5 ((𝜑𝑛 ∈ ω) → ((𝐹‘(inl‘𝑛)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑛)) = 𝐵))
117116adantrr 471 . . . 4 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → ((𝐹‘(inl‘𝑛)) = 𝐵 ∨ ¬ (𝐹‘(inl‘𝑛)) = 𝐵))
11882, 114, 117mpjaodan 788 . . 3 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑚 ∈ ω)) → (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
119118ralrimivva 2518 . 2 (𝜑 → ∀𝑛 ∈ ω ∀𝑚 ∈ ω (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚))
120 difinfsnlem.g . . 3 𝐺 = (𝑛 ∈ ω ↦ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))))
121 2fveq3 5435 . . . . 5 (𝑛 = 𝑚 → (𝐹‘(inl‘𝑛)) = (𝐹‘(inl‘𝑚)))
122121eqeq1d 2149 . . . 4 (𝑛 = 𝑚 → ((𝐹‘(inl‘𝑛)) = 𝐵 ↔ (𝐹‘(inl‘𝑚)) = 𝐵))
123122, 121ifbieq2d 3502 . . 3 (𝑛 = 𝑚 → if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))))
124120, 123f1mpt 5681 . 2 (𝐺:ω–1-1→(𝐴 ∖ {𝐵}) ↔ (∀𝑛 ∈ ω if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) ∈ (𝐴 ∖ {𝐵}) ∧ ∀𝑛 ∈ ω ∀𝑚 ∈ ω (if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))) = if((𝐹‘(inl‘𝑚)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑚))) → 𝑛 = 𝑚)))
12533, 119, 124sylanbrc 414 1 (𝜑𝐺:ω–1-1→(𝐴 ∖ {𝐵}))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   = wceq 1332   ∈ wcel 1481   ≠ wne 2309  ∀wral 2417   ∖ cdif 3074  ∅c0 3369  ifcif 3480  {csn 3533   ↦ cmpt 3998  ωcom 4513  ⟶wf 5128  –1-1→wf1 5129  ‘cfv 5132  1oc1o 6315   ⊔ cdju 6932  inlcinl 6940  inrcinr 6941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140  ax-un 4364 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4224  df-iord 4297  df-on 4299  df-suc 4302  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fv 5140  df-1st 6047  df-1o 6322  df-dju 6933  df-inl 6942  df-inr 6943 This theorem is referenced by:  difinfsn  6995
 Copyright terms: Public domain W3C validator