Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diophrw Structured version   Visualization version   GIF version

Theorem diophrw 37639
Description: Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.)
Assertion
Ref Expression
diophrw ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
Distinct variable groups:   𝑆,𝑎,𝑏,𝑐,𝑑   𝑇,𝑎,𝑏,𝑐,𝑑   𝑀,𝑎,𝑏,𝑐,𝑑   𝑂,𝑎,𝑏,𝑐,𝑑   𝑃,𝑏,𝑐,𝑑
Allowed substitution hint:   𝑃(𝑎)

Proof of Theorem diophrw
StepHypRef Expression
1 simpr 476 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑏 ∈ (ℕ0𝑚 𝑆))
2 nn0ex 11336 . . . . . . . . . . 11 0 ∈ V
3 simp1 1081 . . . . . . . . . . . 12 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
43adantr 480 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑆 ∈ V)
5 elmapg 7912 . . . . . . . . . . 11 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
62, 4, 5sylancr 696 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → (𝑏 ∈ (ℕ0𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
71, 6mpbid 222 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑏:𝑆⟶ℕ0)
87adantr 480 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9 simp2 1082 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇1-1𝑆)
10 f1f 6139 . . . . . . . . . 10 (𝑀:𝑇1-1𝑆𝑀:𝑇𝑆)
119, 10syl 17 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇𝑆)
1211ad2antrr 762 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑀:𝑇𝑆)
13 fco 6096 . . . . . . . 8 ((𝑏:𝑆⟶ℕ0𝑀:𝑇𝑆) → (𝑏𝑀):𝑇⟶ℕ0)
148, 12, 13syl2anc 694 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀):𝑇⟶ℕ0)
15 f1dmex 7178 . . . . . . . . . 10 ((𝑀:𝑇1-1𝑆𝑆 ∈ V) → 𝑇 ∈ V)
169, 3, 15syl2anc 694 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
1716ad2antrr 762 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18 elmapg 7912 . . . . . . . 8 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
192, 17, 18sylancr 696 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
2014, 19mpbird 247 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀) ∈ (ℕ0𝑚 𝑇))
21 simprl 809 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏𝑂))
22 resco 5677 . . . . . . . 8 ((𝑏𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀𝑂))
23 simpll3 1122 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑀𝑂) = ( I ↾ 𝑂))
2423coeq2d 5317 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25 coires1 5691 . . . . . . . . 9 (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏𝑂)
2624, 25syl6eq 2701 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏𝑂))
2722, 26syl5eq 2697 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ↾ 𝑂) = (𝑏𝑂))
2821, 27eqtr4d 2688 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏𝑀) ↾ 𝑂))
29 simpll1 1120 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30 oveq2 6698 . . . . . . . . . . . 12 (𝑎 = 𝑆 → (ℕ0𝑚 𝑎) = (ℕ0𝑚 𝑆))
31 oveq2 6698 . . . . . . . . . . . 12 (𝑎 = 𝑆 → (ℤ ↑𝑚 𝑎) = (ℤ ↑𝑚 𝑆))
3230, 31sseq12d 3667 . . . . . . . . . . 11 (𝑎 = 𝑆 → ((ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎) ↔ (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆)))
33 zex 11424 . . . . . . . . . . . 12 ℤ ∈ V
34 nn0ssz 11436 . . . . . . . . . . . 12 0 ⊆ ℤ
35 mapss 7942 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎))
3633, 34, 35mp2an 708 . . . . . . . . . . 11 (ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎)
3732, 36vtoclg 3297 . . . . . . . . . 10 (𝑆 ∈ V → (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
3829, 37syl 17 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
39 simplr 807 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0𝑚 𝑆))
4038, 39sseldd 3637 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑𝑚 𝑆))
41 coeq1 5312 . . . . . . . . . 10 (𝑑 = 𝑏 → (𝑑𝑀) = (𝑏𝑀))
4241fveq2d 6233 . . . . . . . . 9 (𝑑 = 𝑏 → (𝑃‘(𝑑𝑀)) = (𝑃‘(𝑏𝑀)))
43 eqid 2651 . . . . . . . . 9 (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀))) = (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))
44 fvex 6239 . . . . . . . . 9 (𝑃‘(𝑏𝑀)) ∈ V
4542, 43, 44fvmpt 6321 . . . . . . . 8 (𝑏 ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
4640, 45syl 17 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
47 simprr 811 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)
4846, 47eqtr3d 2687 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏𝑀)) = 0)
49 reseq1 5422 . . . . . . . . 9 (𝑐 = (𝑏𝑀) → (𝑐𝑂) = ((𝑏𝑀) ↾ 𝑂))
5049eqeq2d 2661 . . . . . . . 8 (𝑐 = (𝑏𝑀) → (𝑎 = (𝑐𝑂) ↔ 𝑎 = ((𝑏𝑀) ↾ 𝑂)))
51 fveq2 6229 . . . . . . . . 9 (𝑐 = (𝑏𝑀) → (𝑃𝑐) = (𝑃‘(𝑏𝑀)))
5251eqeq1d 2653 . . . . . . . 8 (𝑐 = (𝑏𝑀) → ((𝑃𝑐) = 0 ↔ (𝑃‘(𝑏𝑀)) = 0))
5350, 52anbi12d 747 . . . . . . 7 (𝑐 = (𝑏𝑀) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) ↔ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)))
5453rspcev 3340 . . . . . 6 (((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ∧ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5520, 28, 48, 54syl12anc 1364 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5655ex 449 . . . 4 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
5756rexlimdva 3060 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
58 simpr 476 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐 ∈ (ℕ0𝑚 𝑇))
5916adantr 480 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑇 ∈ V)
60 elmapg 7912 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
612, 59, 60sylancr 696 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∈ (ℕ0𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
6258, 61mpbid 222 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐:𝑇⟶ℕ0)
6362adantr 480 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
649ad2antrr 762 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:𝑇1-1𝑆)
65 f1cnv 6198 . . . . . . . . . . 11 (𝑀:𝑇1-1𝑆𝑀:ran 𝑀1-1-onto𝑇)
66 f1of 6175 . . . . . . . . . . 11 (𝑀:ran 𝑀1-1-onto𝑇𝑀:ran 𝑀𝑇)
6764, 65, 663syl 18 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:ran 𝑀𝑇)
68 fco 6096 . . . . . . . . . 10 ((𝑐:𝑇⟶ℕ0𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℕ0)
6963, 67, 68syl2anc 694 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℕ0)
70 c0ex 10072 . . . . . . . . . . 11 0 ∈ V
7170fconst 6129 . . . . . . . . . 10 ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
7271a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
73 disjdif 4073 . . . . . . . . . 10 (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
7473a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
75 fun 6104 . . . . . . . . 9 ((((𝑐𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
7669, 72, 74, 75syl21anc 1365 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
77 frn 6091 . . . . . . . . . . . 12 (𝑀:𝑇𝑆 → ran 𝑀𝑆)
789, 10, 773syl 18 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → ran 𝑀𝑆)
7978ad2antrr 762 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ran 𝑀𝑆)
80 undif 4082 . . . . . . . . . 10 (ran 𝑀𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
8179, 80sylib 208 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
82 0nn0 11345 . . . . . . . . . . . 12 0 ∈ ℕ0
83 snssi 4371 . . . . . . . . . . . 12 (0 ∈ ℕ0 → {0} ⊆ ℕ0)
8482, 83ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℕ0
85 ssequn2 3819 . . . . . . . . . . 11 ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
8684, 85mpbi 220 . . . . . . . . . 10 (ℕ0 ∪ {0}) = ℕ0
8786a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℕ0 ∪ {0}) = ℕ0)
8881, 87feq23d 6078 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
8976, 88mpbid 222 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)
90 elmapg 7912 . . . . . . . . 9 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
912, 3, 90sylancr 696 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
9291ad2antrr 762 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
9389, 92mpbird 247 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆))
94 simprl 809 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (𝑐𝑂))
95 resundir 5446 . . . . . . . . . 10 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
96 resco 5677 . . . . . . . . . . . 12 ((𝑐𝑀) ↾ 𝑂) = (𝑐 ∘ (𝑀𝑂))
97 cnvresid 6006 . . . . . . . . . . . . . . 15 ( I ↾ 𝑂) = ( I ↾ 𝑂)
98 simpl2 1085 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑀:𝑇1-1𝑆)
99 df-f1 5931 . . . . . . . . . . . . . . . . . 18 (𝑀:𝑇1-1𝑆 ↔ (𝑀:𝑇𝑆 ∧ Fun 𝑀))
10099simprbi 479 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇1-1𝑆 → Fun 𝑀)
101 funcnvres 6005 . . . . . . . . . . . . . . . . 17 (Fun 𝑀(𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
10298, 100, 1013syl 18 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
103 simpl3 1086 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
104103cnveqd 5330 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
105 df-ima 5156 . . . . . . . . . . . . . . . . . 18 (𝑀𝑂) = ran (𝑀𝑂)
106103rneqd 5385 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) = ran ( I ↾ 𝑂))
107 rnresi 5514 . . . . . . . . . . . . . . . . . . 19 ran ( I ↾ 𝑂) = 𝑂
108106, 107syl6eq 2701 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) = 𝑂)
109105, 108syl5eq 2697 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = 𝑂)
110109reseq2d 5428 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀 ↾ (𝑀𝑂)) = (𝑀𝑂))
111102, 104, 1103eqtr3d 2693 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ( I ↾ 𝑂) = (𝑀𝑂))
11297, 111syl5reqr 2700 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
113112coeq2d 5317 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
114 coires1 5691 . . . . . . . . . . . . 13 (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐𝑂)
115113, 114syl6eq 2701 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐𝑂))
11696, 115syl5eq 2697 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ((𝑐𝑀) ↾ 𝑂) = (𝑐𝑂))
117 dmres 5454 . . . . . . . . . . . . 13 dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
11870snnz 4340 . . . . . . . . . . . . . . . 16 {0} ≠ ∅
119 dmxp 5376 . . . . . . . . . . . . . . . 16 ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
120118, 119ax-mp 5 . . . . . . . . . . . . . . 15 dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
121120ineq2i 3844 . . . . . . . . . . . . . 14 (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
122 inss1 3866 . . . . . . . . . . . . . . . 16 (𝑂𝑆) ⊆ 𝑂
123106, 107syl6req 2702 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑂 = ran (𝑀𝑂))
124 resss 5457 . . . . . . . . . . . . . . . . . 18 (𝑀𝑂) ⊆ 𝑀
125 rnss 5386 . . . . . . . . . . . . . . . . . 18 ((𝑀𝑂) ⊆ 𝑀 → ran (𝑀𝑂) ⊆ ran 𝑀)
126124, 125mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) ⊆ ran 𝑀)
127123, 126eqsstrd 3672 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑂 ⊆ ran 𝑀)
128122, 127syl5ss 3647 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂𝑆) ⊆ ran 𝑀)
129 inssdif0 3980 . . . . . . . . . . . . . . 15 ((𝑂𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
130128, 129sylib 208 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
131121, 130syl5eq 2697 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
132117, 131syl5eq 2697 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
133 relres 5461 . . . . . . . . . . . . 13 Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
134 reldm0 5375 . . . . . . . . . . . . 13 (Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) → ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅))
135133, 134ax-mp 5 . . . . . . . . . . . 12 ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
136132, 135sylibr 224 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
137116, 136uneq12d 3801 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐𝑂) ∪ ∅))
13895, 137syl5eq 2697 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐𝑂) ∪ ∅))
139 un0 4000 . . . . . . . . 9 ((𝑐𝑂) ∪ ∅) = (𝑐𝑂)
140138, 139syl6req 2702 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141140adantr 480 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
14294, 141eqtrd 2685 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
143 fss 6094 . . . . . . . . . . . . . 14 ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
14462, 34, 143sylancl 695 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐:𝑇⟶ℤ)
145144adantr 480 . . . . . . . . . . . 12 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
146 fco 6096 . . . . . . . . . . . 12 ((𝑐:𝑇⟶ℤ ∧ 𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℤ)
147145, 67, 146syl2anc 694 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℤ)
148 fun 6104 . . . . . . . . . . 11 ((((𝑐𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
149147, 72, 74, 148syl21anc 1365 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
150 0z 11426 . . . . . . . . . . . . . 14 0 ∈ ℤ
151 snssi 4371 . . . . . . . . . . . . . 14 (0 ∈ ℤ → {0} ⊆ ℤ)
152150, 151ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℤ
153 ssequn2 3819 . . . . . . . . . . . . 13 ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
154152, 153mpbi 220 . . . . . . . . . . . 12 (ℤ ∪ {0}) = ℤ
155154a1i 11 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
15681, 155feq23d 6078 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
157149, 156mpbid 222 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)
158 elmapg 7912 . . . . . . . . . . 11 ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
15933, 3, 158sylancr 696 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
160159ad2antrr 762 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
161157, 160mpbird 247 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆))
162 coeq1 5312 . . . . . . . . . 10 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑𝑀) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
163162fveq2d 6233 . . . . . . . . 9 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑𝑀)) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164 fvex 6239 . . . . . . . . 9 (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
165163, 43, 164fvmpt 6321 . . . . . . . 8 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
166161, 165syl 17 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
167 coundir 5675 . . . . . . . . 9 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
168 coass 5692 . . . . . . . . . . . 12 ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ (𝑀𝑀))
169 f1cocnv1 6204 . . . . . . . . . . . . . 14 (𝑀:𝑇1-1𝑆 → (𝑀𝑀) = ( I ↾ 𝑇))
170169coeq2d 5317 . . . . . . . . . . . . 13 (𝑀:𝑇1-1𝑆 → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
17164, 170syl 17 . . . . . . . . . . . 12 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
172168, 171syl5eq 2697 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
173120ineq1i 3843 . . . . . . . . . . . . . 14 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
174 incom 3838 . . . . . . . . . . . . . 14 ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
175173, 174, 733eqtri 2677 . . . . . . . . . . . . 13 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
176 coeq0 5682 . . . . . . . . . . . . 13 ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅)
177175, 176mpbir 221 . . . . . . . . . . . 12 (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅
178177a1i 11 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅)
179172, 178uneq12d 3801 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
180 un0 4000 . . . . . . . . . . 11 ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
181 fcoi1 6116 . . . . . . . . . . . 12 (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
18263, 181syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
183180, 182syl5eq 2697 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
184179, 183eqtrd 2685 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
185167, 184syl5eq 2697 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
186185fveq2d 6233 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃𝑐))
187 simprr 811 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃𝑐) = 0)
188166, 186, 1873eqtrd 2689 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
189 reseq1 5422 . . . . . . . . 9 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
190189eqeq2d 2661 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏𝑂) ↔ 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
191 fveq2 6229 . . . . . . . . 9 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))))
192191eqeq1d 2653 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
193190, 192anbi12d 747 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
194193rspcev 3340 . . . . . 6 ((((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ∧ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
19593, 142, 188, 194syl12anc 1364 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
196195ex 449 . . . 4 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
197196rexlimdva 3060 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
19857, 197impbid 202 . 2 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
199198abbidv 2770 1 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wrex 2942  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210  cmpt 4762   I cid 5052   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147  Rel wrel 5148  Fun wfun 5920  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  0cc0 9974  0cn0 11330  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416
This theorem is referenced by:  eldioph2  37642  eldioph2b  37643
  Copyright terms: Public domain W3C validator