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 36802
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 477 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑏 ∈ (ℕ0𝑚 𝑆))
2 nn0ex 11242 . . . . . . . . . . 11 0 ∈ V
3 simp1 1059 . . . . . . . . . . . 12 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
43adantr 481 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑆 ∈ V)
5 elmapg 7815 . . . . . . . . . . 11 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
62, 4, 5sylancr 694 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → (𝑏 ∈ (ℕ0𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
71, 6mpbid 222 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑏:𝑆⟶ℕ0)
87adantr 481 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9 simp2 1060 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇1-1𝑆)
10 f1f 6058 . . . . . . . . . 10 (𝑀:𝑇1-1𝑆𝑀:𝑇𝑆)
119, 10syl 17 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇𝑆)
1211ad2antrr 761 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑀:𝑇𝑆)
13 fco 6015 . . . . . . . 8 ((𝑏:𝑆⟶ℕ0𝑀:𝑇𝑆) → (𝑏𝑀):𝑇⟶ℕ0)
148, 12, 13syl2anc 692 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀):𝑇⟶ℕ0)
15 f1dmex 7083 . . . . . . . . . 10 ((𝑀:𝑇1-1𝑆𝑆 ∈ V) → 𝑇 ∈ V)
169, 3, 15syl2anc 692 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
1716ad2antrr 761 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18 elmapg 7815 . . . . . . . 8 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
192, 17, 18sylancr 694 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
2014, 19mpbird 247 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀) ∈ (ℕ0𝑚 𝑇))
21 simprl 793 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏𝑂))
22 resco 5598 . . . . . . . 8 ((𝑏𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀𝑂))
23 simpll3 1100 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑀𝑂) = ( I ↾ 𝑂))
2423coeq2d 5244 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25 coires1 5612 . . . . . . . . 9 (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏𝑂)
2624, 25syl6eq 2671 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏𝑂))
2722, 26syl5eq 2667 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ↾ 𝑂) = (𝑏𝑂))
2821, 27eqtr4d 2658 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏𝑀) ↾ 𝑂))
29 simpll1 1098 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30 oveq2 6612 . . . . . . . . . . . 12 (𝑎 = 𝑆 → (ℕ0𝑚 𝑎) = (ℕ0𝑚 𝑆))
31 oveq2 6612 . . . . . . . . . . . 12 (𝑎 = 𝑆 → (ℤ ↑𝑚 𝑎) = (ℤ ↑𝑚 𝑆))
3230, 31sseq12d 3613 . . . . . . . . . . 11 (𝑎 = 𝑆 → ((ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎) ↔ (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆)))
33 zex 11330 . . . . . . . . . . . 12 ℤ ∈ V
34 nn0ssz 11342 . . . . . . . . . . . 12 0 ⊆ ℤ
35 mapss 7844 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎))
3633, 34, 35mp2an 707 . . . . . . . . . . 11 (ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎)
3732, 36vtoclg 3252 . . . . . . . . . 10 (𝑆 ∈ V → (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
3829, 37syl 17 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
39 simplr 791 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0𝑚 𝑆))
4038, 39sseldd 3584 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑𝑚 𝑆))
41 coeq1 5239 . . . . . . . . . 10 (𝑑 = 𝑏 → (𝑑𝑀) = (𝑏𝑀))
4241fveq2d 6152 . . . . . . . . 9 (𝑑 = 𝑏 → (𝑃‘(𝑑𝑀)) = (𝑃‘(𝑏𝑀)))
43 eqid 2621 . . . . . . . . 9 (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀))) = (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))
44 fvex 6158 . . . . . . . . 9 (𝑃‘(𝑏𝑀)) ∈ V
4542, 43, 44fvmpt 6239 . . . . . . . 8 (𝑏 ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
4640, 45syl 17 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
47 simprr 795 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)
4846, 47eqtr3d 2657 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏𝑀)) = 0)
49 reseq1 5350 . . . . . . . . 9 (𝑐 = (𝑏𝑀) → (𝑐𝑂) = ((𝑏𝑀) ↾ 𝑂))
5049eqeq2d 2631 . . . . . . . 8 (𝑐 = (𝑏𝑀) → (𝑎 = (𝑐𝑂) ↔ 𝑎 = ((𝑏𝑀) ↾ 𝑂)))
51 fveq2 6148 . . . . . . . . 9 (𝑐 = (𝑏𝑀) → (𝑃𝑐) = (𝑃‘(𝑏𝑀)))
5251eqeq1d 2623 . . . . . . . 8 (𝑐 = (𝑏𝑀) → ((𝑃𝑐) = 0 ↔ (𝑃‘(𝑏𝑀)) = 0))
5350, 52anbi12d 746 . . . . . . 7 (𝑐 = (𝑏𝑀) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) ↔ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)))
5453rspcev 3295 . . . . . 6 (((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ∧ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5520, 28, 48, 54syl12anc 1321 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5655ex 450 . . . 4 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
5756rexlimdva 3024 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
58 simpr 477 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐 ∈ (ℕ0𝑚 𝑇))
5916adantr 481 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑇 ∈ V)
60 elmapg 7815 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
612, 59, 60sylancr 694 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∈ (ℕ0𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
6258, 61mpbid 222 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐:𝑇⟶ℕ0)
6362adantr 481 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
649ad2antrr 761 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:𝑇1-1𝑆)
65 f1cnv 6117 . . . . . . . . . . 11 (𝑀:𝑇1-1𝑆𝑀:ran 𝑀1-1-onto𝑇)
66 f1of 6094 . . . . . . . . . . 11 (𝑀:ran 𝑀1-1-onto𝑇𝑀:ran 𝑀𝑇)
6764, 65, 663syl 18 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:ran 𝑀𝑇)
68 fco 6015 . . . . . . . . . 10 ((𝑐:𝑇⟶ℕ0𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℕ0)
6963, 67, 68syl2anc 692 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℕ0)
70 c0ex 9978 . . . . . . . . . . 11 0 ∈ V
7170fconst 6048 . . . . . . . . . 10 ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
7271a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
73 disjdif 4012 . . . . . . . . . 10 (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
7473a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
75 fun 6023 . . . . . . . . 9 ((((𝑐𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
7669, 72, 74, 75syl21anc 1322 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
77 frn 6010 . . . . . . . . . . . 12 (𝑀:𝑇𝑆 → ran 𝑀𝑆)
789, 10, 773syl 18 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → ran 𝑀𝑆)
7978ad2antrr 761 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ran 𝑀𝑆)
80 undif 4021 . . . . . . . . . 10 (ran 𝑀𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
8179, 80sylib 208 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
82 0nn0 11251 . . . . . . . . . . . 12 0 ∈ ℕ0
83 snssi 4308 . . . . . . . . . . . 12 (0 ∈ ℕ0 → {0} ⊆ ℕ0)
8482, 83ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℕ0
85 ssequn2 3764 . . . . . . . . . . 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 5997 . . . . . . . 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 7815 . . . . . . . . 9 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
912, 3, 90sylancr 694 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
9291ad2antrr 761 . . . . . . 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 793 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (𝑐𝑂))
95 resundir 5370 . . . . . . . . . 10 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
96 resco 5598 . . . . . . . . . . . 12 ((𝑐𝑀) ↾ 𝑂) = (𝑐 ∘ (𝑀𝑂))
97 cnvresid 5926 . . . . . . . . . . . . . . 15 ( I ↾ 𝑂) = ( I ↾ 𝑂)
98 simpl2 1063 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑀:𝑇1-1𝑆)
99 df-f1 5852 . . . . . . . . . . . . . . . . . 18 (𝑀:𝑇1-1𝑆 ↔ (𝑀:𝑇𝑆 ∧ Fun 𝑀))
10099simprbi 480 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇1-1𝑆 → Fun 𝑀)
101 funcnvres 5925 . . . . . . . . . . . . . . . . 17 (Fun 𝑀(𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
10298, 100, 1013syl 18 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
103 simpl3 1064 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
104103cnveqd 5258 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
105 df-ima 5087 . . . . . . . . . . . . . . . . . 18 (𝑀𝑂) = ran (𝑀𝑂)
106103rneqd 5313 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) = ran ( I ↾ 𝑂))
107 rnresi 5438 . . . . . . . . . . . . . . . . . . 19 ran ( I ↾ 𝑂) = 𝑂
108106, 107syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) = 𝑂)
109105, 108syl5eq 2667 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = 𝑂)
110109reseq2d 5356 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀 ↾ (𝑀𝑂)) = (𝑀𝑂))
111102, 104, 1103eqtr3d 2663 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ( I ↾ 𝑂) = (𝑀𝑂))
11297, 111syl5reqr 2670 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
113112coeq2d 5244 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
114 coires1 5612 . . . . . . . . . . . . 13 (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐𝑂)
115113, 114syl6eq 2671 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐𝑂))
11696, 115syl5eq 2667 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ((𝑐𝑀) ↾ 𝑂) = (𝑐𝑂))
117 dmres 5378 . . . . . . . . . . . . 13 dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
11870snnz 4279 . . . . . . . . . . . . . . . 16 {0} ≠ ∅
119 dmxp 5304 . . . . . . . . . . . . . . . 16 ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
120118, 119ax-mp 5 . . . . . . . . . . . . . . 15 dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
121120ineq2i 3789 . . . . . . . . . . . . . 14 (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
122 inss1 3811 . . . . . . . . . . . . . . . 16 (𝑂𝑆) ⊆ 𝑂
123106, 107syl6req 2672 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑂 = ran (𝑀𝑂))
124 resss 5381 . . . . . . . . . . . . . . . . . 18 (𝑀𝑂) ⊆ 𝑀
125 rnss 5314 . . . . . . . . . . . . . . . . . 18 ((𝑀𝑂) ⊆ 𝑀 → ran (𝑀𝑂) ⊆ ran 𝑀)
126124, 125mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) ⊆ ran 𝑀)
127123, 126eqsstrd 3618 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑂 ⊆ ran 𝑀)
128122, 127syl5ss 3594 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂𝑆) ⊆ ran 𝑀)
129 inssdif0 3921 . . . . . . . . . . . . . . 15 ((𝑂𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
130128, 129sylib 208 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
131121, 130syl5eq 2667 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
132117, 131syl5eq 2667 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
133 relres 5385 . . . . . . . . . . . . 13 Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
134 reldm0 5303 . . . . . . . . . . . . 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 3746 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐𝑂) ∪ ∅))
13895, 137syl5eq 2667 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐𝑂) ∪ ∅))
139 un0 3939 . . . . . . . . 9 ((𝑐𝑂) ∪ ∅) = (𝑐𝑂)
140138, 139syl6req 2672 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141140adantr 481 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
14294, 141eqtrd 2655 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
143 fss 6013 . . . . . . . . . . . . . 14 ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
14462, 34, 143sylancl 693 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐:𝑇⟶ℤ)
145144adantr 481 . . . . . . . . . . . 12 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
146 fco 6015 . . . . . . . . . . . 12 ((𝑐:𝑇⟶ℤ ∧ 𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℤ)
147145, 67, 146syl2anc 692 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℤ)
148 fun 6023 . . . . . . . . . . 11 ((((𝑐𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
149147, 72, 74, 148syl21anc 1322 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
150 0z 11332 . . . . . . . . . . . . . 14 0 ∈ ℤ
151 snssi 4308 . . . . . . . . . . . . . 14 (0 ∈ ℤ → {0} ⊆ ℤ)
152150, 151ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℤ
153 ssequn2 3764 . . . . . . . . . . . . 13 ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
154152, 153mpbi 220 . . . . . . . . . . . 12 (ℤ ∪ {0}) = ℤ
155154a1i 11 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
15681, 155feq23d 5997 . . . . . . . . . 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 7815 . . . . . . . . . . 11 ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
15933, 3, 158sylancr 694 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
160159ad2antrr 761 . . . . . . . . 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 5239 . . . . . . . . . 10 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑𝑀) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
163162fveq2d 6152 . . . . . . . . 9 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑𝑀)) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164 fvex 6158 . . . . . . . . 9 (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
165163, 43, 164fvmpt 6239 . . . . . . . 8 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
166161, 165syl 17 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
167 coundir 5596 . . . . . . . . 9 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
168 coass 5613 . . . . . . . . . . . 12 ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ (𝑀𝑀))
169 f1cocnv1 6123 . . . . . . . . . . . . . 14 (𝑀:𝑇1-1𝑆 → (𝑀𝑀) = ( I ↾ 𝑇))
170169coeq2d 5244 . . . . . . . . . . . . 13 (𝑀:𝑇1-1𝑆 → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
17164, 170syl 17 . . . . . . . . . . . 12 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
172168, 171syl5eq 2667 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
173120ineq1i 3788 . . . . . . . . . . . . . 14 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
174 incom 3783 . . . . . . . . . . . . . 14 ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
175173, 174, 733eqtri 2647 . . . . . . . . . . . . 13 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
176 coeq0 5603 . . . . . . . . . . . . 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 3746 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
180 un0 3939 . . . . . . . . . . 11 ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
181 fcoi1 6035 . . . . . . . . . . . 12 (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
18263, 181syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
183180, 182syl5eq 2667 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
184179, 183eqtrd 2655 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
185167, 184syl5eq 2667 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
186185fveq2d 6152 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃𝑐))
187 simprr 795 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃𝑐) = 0)
188166, 186, 1873eqtrd 2659 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
189 reseq1 5350 . . . . . . . . 9 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
190189eqeq2d 2631 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏𝑂) ↔ 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
191 fveq2 6148 . . . . . . . . 9 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))))
192191eqeq1d 2623 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
193190, 192anbi12d 746 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
194193rspcev 3295 . . . . . 6 ((((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ∧ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
19593, 142, 188, 194syl12anc 1321 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
196195ex 450 . . . 4 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
197196rexlimdva 3024 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
19857, 197impbid 202 . 2 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
199198abbidv 2738 1 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  {cab 2607  wne 2790  wrex 2908  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  {csn 4148  cmpt 4673   I cid 4984   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  ccom 5078  Rel wrel 5079  Fun wfun 5841  wf 5843  1-1wf1 5844  1-1-ontowf1o 5846  cfv 5847  (class class class)co 6604  𝑚 cmap 7802  0cc0 9880  0cn0 11236  cz 11321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-n0 11237  df-z 11322
This theorem is referenced by:  eldioph2  36805  eldioph2b  36806
  Copyright terms: Public domain W3C validator