Metamath Proof Explorer


Theorem actfunsnrndisj

Description: The action F of extending function from B to C with new values at point I yields different functions. (Contributed by Thierry Arnoux, 9-Dec-2021)

Ref Expression
Hypotheses actfunsn.1 ( ( 𝜑𝑘𝐶 ) → 𝐴 ⊆ ( 𝐶m 𝐵 ) )
actfunsn.2 ( 𝜑𝐶 ∈ V )
actfunsn.3 ( 𝜑𝐼𝑉 )
actfunsn.4 ( 𝜑 → ¬ 𝐼𝐵 )
actfunsn.5 𝐹 = ( 𝑥𝐴 ↦ ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
Assertion actfunsnrndisj ( 𝜑Disj 𝑘𝐶 ran 𝐹 )

Proof

Step Hyp Ref Expression
1 actfunsn.1 ( ( 𝜑𝑘𝐶 ) → 𝐴 ⊆ ( 𝐶m 𝐵 ) )
2 actfunsn.2 ( 𝜑𝐶 ∈ V )
3 actfunsn.3 ( 𝜑𝐼𝑉 )
4 actfunsn.4 ( 𝜑 → ¬ 𝐼𝐵 )
5 actfunsn.5 𝐹 = ( 𝑥𝐴 ↦ ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
6 simpr ( ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) ∧ 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
7 6 fveq1d ( ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) ∧ 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑓𝐼 ) = ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ‘ 𝐼 ) )
8 1 ad2antrr ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝐴 ⊆ ( 𝐶m 𝐵 ) )
9 simpr ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝑧𝐴 )
10 8 9 sseldd ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝑧 ∈ ( 𝐶m 𝐵 ) )
11 elmapfn ( 𝑧 ∈ ( 𝐶m 𝐵 ) → 𝑧 Fn 𝐵 )
12 10 11 syl ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝑧 Fn 𝐵 )
13 3 ad3antrrr ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝐼𝑉 )
14 simpllr ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝑘𝐶 )
15 fnsng ( ( 𝐼𝑉𝑘𝐶 ) → { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } )
16 13 14 15 syl2anc ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } )
17 disjsn ( ( 𝐵 ∩ { 𝐼 } ) = ∅ ↔ ¬ 𝐼𝐵 )
18 4 17 sylibr ( 𝜑 → ( 𝐵 ∩ { 𝐼 } ) = ∅ )
19 18 ad3antrrr ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → ( 𝐵 ∩ { 𝐼 } ) = ∅ )
20 snidg ( 𝐼𝑉𝐼 ∈ { 𝐼 } )
21 13 20 syl ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → 𝐼 ∈ { 𝐼 } )
22 fvun2 ( ( 𝑧 Fn 𝐵 ∧ { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } ∧ ( ( 𝐵 ∩ { 𝐼 } ) = ∅ ∧ 𝐼 ∈ { 𝐼 } ) ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ‘ 𝐼 ) = ( { ⟨ 𝐼 , 𝑘 ⟩ } ‘ 𝐼 ) )
23 12 16 19 21 22 syl112anc ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ‘ 𝐼 ) = ( { ⟨ 𝐼 , 𝑘 ⟩ } ‘ 𝐼 ) )
24 fvsng ( ( 𝐼𝑉𝑘𝐶 ) → ( { ⟨ 𝐼 , 𝑘 ⟩ } ‘ 𝐼 ) = 𝑘 )
25 13 14 24 syl2anc ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → ( { ⟨ 𝐼 , 𝑘 ⟩ } ‘ 𝐼 ) = 𝑘 )
26 23 25 eqtrd ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ‘ 𝐼 ) = 𝑘 )
27 26 adantr ( ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) ∧ 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ‘ 𝐼 ) = 𝑘 )
28 7 27 eqtrd ( ( ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) ∧ 𝑧𝐴 ) ∧ 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑓𝐼 ) = 𝑘 )
29 simpr ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) → 𝑓 ∈ ran 𝐹 )
30 uneq1 ( 𝑥 = 𝑧 → ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
31 30 cbvmptv ( 𝑥𝐴 ↦ ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) = ( 𝑧𝐴 ↦ ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
32 5 31 eqtri 𝐹 = ( 𝑧𝐴 ↦ ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
33 vex 𝑧 ∈ V
34 snex { ⟨ 𝐼 , 𝑘 ⟩ } ∈ V
35 33 34 unex ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ∈ V
36 32 35 elrnmpti ( 𝑓 ∈ ran 𝐹 ↔ ∃ 𝑧𝐴 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
37 29 36 sylib ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) → ∃ 𝑧𝐴 𝑓 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
38 28 37 r19.29a ( ( ( 𝜑𝑘𝐶 ) ∧ 𝑓 ∈ ran 𝐹 ) → ( 𝑓𝐼 ) = 𝑘 )
39 38 ralrimiva ( ( 𝜑𝑘𝐶 ) → ∀ 𝑓 ∈ ran 𝐹 ( 𝑓𝐼 ) = 𝑘 )
40 39 ralrimiva ( 𝜑 → ∀ 𝑘𝐶𝑓 ∈ ran 𝐹 ( 𝑓𝐼 ) = 𝑘 )
41 invdisj ( ∀ 𝑘𝐶𝑓 ∈ ran 𝐹 ( 𝑓𝐼 ) = 𝑘Disj 𝑘𝐶 ran 𝐹 )
42 40 41 syl ( 𝜑Disj 𝑘𝐶 ran 𝐹 )