Metamath Proof Explorer

Theorem noseponlem

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

Ref Expression
Assertion noseponlem ⊢ A ∈ No ∧ B ∈ No ∧ dom ⁡ A ∈ dom ⁡ B → ¬ ∀ x ∈ On A ⁡ x = B ⁡ x

Proof

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