Theorem noseponlem

Description: Lemma for nosepon . Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020)

	Ref	Expression
Assertion	noseponlem	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		nodmon	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → dom 𝐴 ∈ On )
3		nodmord	⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
4		ordirr	⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
5	3 4	syl	⊢ ( 𝐴 ∈ No → ¬ dom 𝐴 ∈ dom 𝐴 )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ¬ dom 𝐴 ∈ dom 𝐴 )
7		ndmfv	⊢ ( ¬ dom 𝐴 ∈ dom 𝐴 → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
8	6 7	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
9		nosgnn0	⊢ ¬ ∅ ∈ { 1o , 2o }
10		elno3	⊢ ( 𝐵 ∈ No ↔ ( 𝐵 : dom 𝐵 ⟶ { 1o , 2o } ∧ dom 𝐵 ∈ On ) )
11	10	simplbi	⊢ ( 𝐵 ∈ No → 𝐵 : dom 𝐵 ⟶ { 1o , 2o } )
12	11	3ad2ant2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → 𝐵 : dom 𝐵 ⟶ { 1o , 2o } )
13		simp3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → dom 𝐴 ∈ dom 𝐵 )
14	12 13	ffvelrnd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ dom 𝐴 ) ∈ { 1o , 2o } )
15		eleq1	⊢ ( ( 𝐵 ‘ dom 𝐴 ) = ∅ → ( ( 𝐵 ‘ dom 𝐴 ) ∈ { 1o , 2o } ↔ ∅ ∈ { 1o , 2o } ) )
16	14 15	syl5ibcom	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ( ( 𝐵 ‘ dom 𝐴 ) = ∅ → ∅ ∈ { 1o , 2o } ) )
17	9 16	mtoi	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ¬ ( 𝐵 ‘ dom 𝐴 ) = ∅ )
18	17	neqned	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ( 𝐵 ‘ dom 𝐴 ) ≠ ∅ )
19	18	necomd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ∅ ≠ ( 𝐵 ‘ dom 𝐴 ) )
20	8 19	eqnetrd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ( 𝐴 ‘ dom 𝐴 ) ≠ ( 𝐵 ‘ dom 𝐴 ) )
21		fveq2	⊢ ( 𝑥 = dom 𝐴 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ dom 𝐴 ) )
22		fveq2	⊢ ( 𝑥 = dom 𝐴 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ dom 𝐴 ) )
23	21 22	neeq12d	⊢ ( 𝑥 = dom 𝐴 → ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐴 ‘ dom 𝐴 ) ≠ ( 𝐵 ‘ dom 𝐴 ) ) )
24	23	rspcev	⊢ ( ( dom 𝐴 ∈ On ∧ ( 𝐴 ‘ dom 𝐴 ) ≠ ( 𝐵 ‘ dom 𝐴 ) ) → ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) )
25	2 20 24	syl2anc	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) )
26		df-ne	⊢ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
27	26	rexbii	⊢ ( ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
28		rexnal	⊢ ( ∃ 𝑥 ∈ On ¬ ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
29	27 28	bitri	⊢ ( ∃ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) ≠ ( 𝐵 ‘ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
30	25 29	sylib	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵 ) → ¬ ∀ 𝑥 ∈ On ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )