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 𝐹 )