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 37824
 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 479 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑏 ∈ (ℕ0𝑚 𝑆))
2 nn0ex 11490 . . . . . . . . . . 11 0 ∈ V
3 simp1 1131 . . . . . . . . . . . 12 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
43adantr 472 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑆 ∈ V)
5 elmapg 8036 . . . . . . . . . . 11 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
62, 4, 5sylancr 698 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → (𝑏 ∈ (ℕ0𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
71, 6mpbid 222 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → 𝑏:𝑆⟶ℕ0)
87adantr 472 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9 simp2 1132 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇1-1𝑆)
10 f1f 6262 . . . . . . . . . 10 (𝑀:𝑇1-1𝑆𝑀:𝑇𝑆)
119, 10syl 17 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇𝑆)
1211ad2antrr 764 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑀:𝑇𝑆)
13 fco 6219 . . . . . . . 8 ((𝑏:𝑆⟶ℕ0𝑀:𝑇𝑆) → (𝑏𝑀):𝑇⟶ℕ0)
148, 12, 13syl2anc 696 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀):𝑇⟶ℕ0)
15 f1dmex 7301 . . . . . . . . . 10 ((𝑀:𝑇1-1𝑆𝑆 ∈ V) → 𝑇 ∈ V)
169, 3, 15syl2anc 696 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
1716ad2antrr 764 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18 elmapg 8036 . . . . . . . 8 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
192, 17, 18sylancr 698 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
2014, 19mpbird 247 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀) ∈ (ℕ0𝑚 𝑇))
21 simprl 811 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏𝑂))
22 resco 5800 . . . . . . . 8 ((𝑏𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀𝑂))
23 simpll3 1259 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑀𝑂) = ( I ↾ 𝑂))
2423coeq2d 5440 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25 coires1 5814 . . . . . . . . 9 (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏𝑂)
2624, 25syl6eq 2810 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏𝑂))
2722, 26syl5eq 2806 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ↾ 𝑂) = (𝑏𝑂))
2821, 27eqtr4d 2797 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏𝑀) ↾ 𝑂))
29 simpll1 1255 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30 oveq2 6821 . . . . . . . . . . . 12 (𝑎 = 𝑆 → (ℕ0𝑚 𝑎) = (ℕ0𝑚 𝑆))
31 oveq2 6821 . . . . . . . . . . . 12 (𝑎 = 𝑆 → (ℤ ↑𝑚 𝑎) = (ℤ ↑𝑚 𝑆))
3230, 31sseq12d 3775 . . . . . . . . . . 11 (𝑎 = 𝑆 → ((ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎) ↔ (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆)))
33 zex 11578 . . . . . . . . . . . 12 ℤ ∈ V
34 nn0ssz 11590 . . . . . . . . . . . 12 0 ⊆ ℤ
35 mapss 8066 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎))
3633, 34, 35mp2an 710 . . . . . . . . . . 11 (ℕ0𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎)
3732, 36vtoclg 3406 . . . . . . . . . 10 (𝑆 ∈ V → (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
3829, 37syl 17 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (ℕ0𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
39 simplr 809 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0𝑚 𝑆))
4038, 39sseldd 3745 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑𝑚 𝑆))
41 coeq1 5435 . . . . . . . . . 10 (𝑑 = 𝑏 → (𝑑𝑀) = (𝑏𝑀))
4241fveq2d 6356 . . . . . . . . 9 (𝑑 = 𝑏 → (𝑃‘(𝑑𝑀)) = (𝑃‘(𝑏𝑀)))
43 eqid 2760 . . . . . . . . 9 (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀))) = (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))
44 fvex 6362 . . . . . . . . 9 (𝑃‘(𝑏𝑀)) ∈ V
4542, 43, 44fvmpt 6444 . . . . . . . 8 (𝑏 ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
4640, 45syl 17 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
47 simprr 813 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)
4846, 47eqtr3d 2796 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏𝑀)) = 0)
49 reseq1 5545 . . . . . . . . 9 (𝑐 = (𝑏𝑀) → (𝑐𝑂) = ((𝑏𝑀) ↾ 𝑂))
5049eqeq2d 2770 . . . . . . . 8 (𝑐 = (𝑏𝑀) → (𝑎 = (𝑐𝑂) ↔ 𝑎 = ((𝑏𝑀) ↾ 𝑂)))
51 fveq2 6352 . . . . . . . . 9 (𝑐 = (𝑏𝑀) → (𝑃𝑐) = (𝑃‘(𝑏𝑀)))
5251eqeq1d 2762 . . . . . . . 8 (𝑐 = (𝑏𝑀) → ((𝑃𝑐) = 0 ↔ (𝑃‘(𝑏𝑀)) = 0))
5350, 52anbi12d 749 . . . . . . 7 (𝑐 = (𝑏𝑀) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) ↔ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)))
5453rspcev 3449 . . . . . 6 (((𝑏𝑀) ∈ (ℕ0𝑚 𝑇) ∧ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5520, 28, 48, 54syl12anc 1475 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5655ex 449 . . . 4 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0𝑚 𝑆)) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
5756rexlimdva 3169 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
58 simpr 479 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐 ∈ (ℕ0𝑚 𝑇))
5916adantr 472 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑇 ∈ V)
60 elmapg 8036 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
612, 59, 60sylancr 698 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∈ (ℕ0𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
6258, 61mpbid 222 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐:𝑇⟶ℕ0)
6362adantr 472 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
649ad2antrr 764 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:𝑇1-1𝑆)
65 f1cnv 6321 . . . . . . . . . . 11 (𝑀:𝑇1-1𝑆𝑀:ran 𝑀1-1-onto𝑇)
66 f1of 6298 . . . . . . . . . . 11 (𝑀:ran 𝑀1-1-onto𝑇𝑀:ran 𝑀𝑇)
6764, 65, 663syl 18 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:ran 𝑀𝑇)
68 fco 6219 . . . . . . . . . 10 ((𝑐:𝑇⟶ℕ0𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℕ0)
6963, 67, 68syl2anc 696 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℕ0)
70 c0ex 10226 . . . . . . . . . . 11 0 ∈ V
7170fconst 6252 . . . . . . . . . 10 ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
7271a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
73 disjdif 4184 . . . . . . . . . 10 (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
7473a1i 11 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
75 fun 6227 . . . . . . . . 9 ((((𝑐𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
7669, 72, 74, 75syl21anc 1476 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
77 frn 6214 . . . . . . . . . . . 12 (𝑀:𝑇𝑆 → ran 𝑀𝑆)
789, 10, 773syl 18 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → ran 𝑀𝑆)
7978ad2antrr 764 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ran 𝑀𝑆)
80 undif 4193 . . . . . . . . . 10 (ran 𝑀𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
8179, 80sylib 208 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
82 0nn0 11499 . . . . . . . . . . . 12 0 ∈ ℕ0
83 snssi 4484 . . . . . . . . . . . 12 (0 ∈ ℕ0 → {0} ⊆ ℕ0)
8482, 83ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℕ0
85 ssequn2 3929 . . . . . . . . . . 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 6201 . . . . . . . 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 8036 . . . . . . . . 9 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
912, 3, 90sylancr 698 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
9291ad2antrr 764 . . . . . . 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 811 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (𝑐𝑂))
95 resundir 5569 . . . . . . . . . 10 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
96 resco 5800 . . . . . . . . . . . 12 ((𝑐𝑀) ↾ 𝑂) = (𝑐 ∘ (𝑀𝑂))
97 cnvresid 6129 . . . . . . . . . . . . . . 15 ( I ↾ 𝑂) = ( I ↾ 𝑂)
98 simpl2 1230 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑀:𝑇1-1𝑆)
99 df-f1 6054 . . . . . . . . . . . . . . . . . 18 (𝑀:𝑇1-1𝑆 ↔ (𝑀:𝑇𝑆 ∧ Fun 𝑀))
10099simprbi 483 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇1-1𝑆 → Fun 𝑀)
101 funcnvres 6128 . . . . . . . . . . . . . . . . 17 (Fun 𝑀(𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
10298, 100, 1013syl 18 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
103 simpl3 1232 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
104103cnveqd 5453 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
105 df-ima 5279 . . . . . . . . . . . . . . . . . 18 (𝑀𝑂) = ran (𝑀𝑂)
106103rneqd 5508 . . . . . . . . . . . . . . . . . . 19 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) = ran ( I ↾ 𝑂))
107 rnresi 5637 . . . . . . . . . . . . . . . . . . 19 ran ( I ↾ 𝑂) = 𝑂
108106, 107syl6eq 2810 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) = 𝑂)
109105, 108syl5eq 2806 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = 𝑂)
110109reseq2d 5551 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀 ↾ (𝑀𝑂)) = (𝑀𝑂))
111102, 104, 1103eqtr3d 2802 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ( I ↾ 𝑂) = (𝑀𝑂))
11297, 111syl5reqr 2809 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
113112coeq2d 5440 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
114 coires1 5814 . . . . . . . . . . . . 13 (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐𝑂)
115113, 114syl6eq 2810 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐𝑂))
11696, 115syl5eq 2806 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ((𝑐𝑀) ↾ 𝑂) = (𝑐𝑂))
117 dmres 5577 . . . . . . . . . . . . 13 dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
11870snnz 4452 . . . . . . . . . . . . . . . 16 {0} ≠ ∅
119 dmxp 5499 . . . . . . . . . . . . . . . 16 ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
120118, 119ax-mp 5 . . . . . . . . . . . . . . 15 dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
121120ineq2i 3954 . . . . . . . . . . . . . 14 (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
122 inss1 3976 . . . . . . . . . . . . . . . 16 (𝑂𝑆) ⊆ 𝑂
123106, 107syl6req 2811 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑂 = ran (𝑀𝑂))
124 resss 5580 . . . . . . . . . . . . . . . . . 18 (𝑀𝑂) ⊆ 𝑀
125 rnss 5509 . . . . . . . . . . . . . . . . . 18 ((𝑀𝑂) ⊆ 𝑀 → ran (𝑀𝑂) ⊆ ran 𝑀)
126124, 125mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ran (𝑀𝑂) ⊆ ran 𝑀)
127123, 126eqsstrd 3780 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑂 ⊆ ran 𝑀)
128122, 127syl5ss 3755 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂𝑆) ⊆ ran 𝑀)
129 inssdif0 4090 . . . . . . . . . . . . . . 15 ((𝑂𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
130128, 129sylib 208 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
131121, 130syl5eq 2806 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
132117, 131syl5eq 2806 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
133 relres 5584 . . . . . . . . . . . . 13 Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
134 reldm0 5498 . . . . . . . . . . . . 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 3911 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐𝑂) ∪ ∅))
13895, 137syl5eq 2806 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐𝑂) ∪ ∅))
139 un0 4110 . . . . . . . . 9 ((𝑐𝑂) ∪ ∅) = (𝑐𝑂)
140138, 139syl6req 2811 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141140adantr 472 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
14294, 141eqtrd 2794 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
143 fss 6217 . . . . . . . . . . . . . 14 ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
14462, 34, 143sylancl 697 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → 𝑐:𝑇⟶ℤ)
145144adantr 472 . . . . . . . . . . . 12 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
146 fco 6219 . . . . . . . . . . . 12 ((𝑐:𝑇⟶ℤ ∧ 𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℤ)
147145, 67, 146syl2anc 696 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℤ)
148 fun 6227 . . . . . . . . . . 11 ((((𝑐𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
149147, 72, 74, 148syl21anc 1476 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
150 0z 11580 . . . . . . . . . . . . . 14 0 ∈ ℤ
151 snssi 4484 . . . . . . . . . . . . . 14 (0 ∈ ℤ → {0} ⊆ ℤ)
152150, 151ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℤ
153 ssequn2 3929 . . . . . . . . . . . . 13 ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
154152, 153mpbi 220 . . . . . . . . . . . 12 (ℤ ∪ {0}) = ℤ
155154a1i 11 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
15681, 155feq23d 6201 . . . . . . . . . 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 8036 . . . . . . . . . . 11 ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
15933, 3, 158sylancr 698 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
160159ad2antrr 764 . . . . . . . . 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 5435 . . . . . . . . . 10 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑𝑀) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
163162fveq2d 6356 . . . . . . . . 9 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑𝑀)) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164 fvex 6362 . . . . . . . . 9 (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
165163, 43, 164fvmpt 6444 . . . . . . . 8 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
166161, 165syl 17 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
167 coundir 5798 . . . . . . . . 9 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
168 coass 5815 . . . . . . . . . . . 12 ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ (𝑀𝑀))
169 f1cocnv1 6327 . . . . . . . . . . . . . 14 (𝑀:𝑇1-1𝑆 → (𝑀𝑀) = ( I ↾ 𝑇))
170169coeq2d 5440 . . . . . . . . . . . . 13 (𝑀:𝑇1-1𝑆 → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
17164, 170syl 17 . . . . . . . . . . . 12 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
172168, 171syl5eq 2806 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
173120ineq1i 3953 . . . . . . . . . . . . . 14 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
174 incom 3948 . . . . . . . . . . . . . 14 ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
175173, 174, 733eqtri 2786 . . . . . . . . . . . . 13 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
176 coeq0 5805 . . . . . . . . . . . . 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 3911 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
180 un0 4110 . . . . . . . . . . 11 ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
181 fcoi1 6239 . . . . . . . . . . . 12 (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
18263, 181syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
183180, 182syl5eq 2806 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
184179, 183eqtrd 2794 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
185167, 184syl5eq 2806 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
186185fveq2d 6356 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃𝑐))
187 simprr 813 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃𝑐) = 0)
188166, 186, 1873eqtrd 2798 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
189 reseq1 5545 . . . . . . . . 9 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
190189eqeq2d 2770 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏𝑂) ↔ 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
191 fveq2 6352 . . . . . . . . 9 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))))
192191eqeq1d 2762 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
193190, 192anbi12d 749 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
194193rspcev 3449 . . . . . 6 ((((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0𝑚 𝑆) ∧ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
19593, 142, 188, 194syl12anc 1475 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
196195ex 449 . . . 4 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0𝑚 𝑇)) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
197196rexlimdva 3169 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
19857, 197impbid 202 . 2 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
199198abbidv 2879 1 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0𝑚 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0𝑚 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  {cab 2746   ≠ wne 2932  ∃wrex 3051  Vcvv 3340   ∖ cdif 3712   ∪ cun 3713   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058  {csn 4321   ↦ cmpt 4881   I cid 5173   × cxp 5264  ◡ccnv 5265  dom cdm 5266  ran crn 5267   ↾ cres 5268   “ cima 5269   ∘ ccom 5270  Rel wrel 5271  Fun wfun 6043  ⟶wf 6045  –1-1→wf1 6046  –1-1-onto→wf1o 6048  ‘cfv 6049  (class class class)co 6813   ↑𝑚 cmap 8023  0cc0 10128  ℕ0cn0 11484  ℤcz 11569 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570 This theorem is referenced by:  eldioph2  37827  eldioph2b  37828
 Copyright terms: Public domain W3C validator