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∈OnA⁡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∈OnA⁡x≠B⁡x
25 2 20 24 syl2anc ⊢A∈No∧B∈No∧dom⁡A∈dom⁡B→∃x∈OnA⁡x≠B⁡x
26 df-ne ⊢A⁡x≠B⁡x↔¬A⁡x=B⁡x
27 26 rexbii ⊢∃x∈OnA⁡x≠B⁡x↔∃x∈On¬A⁡x=B⁡x
28 rexnal ⊢∃x∈On¬A⁡x=B⁡x↔¬∀x∈OnA⁡x=B⁡x
29 27 28 bitri ⊢∃x∈OnA⁡x≠B⁡x↔¬∀x∈OnA⁡x=B⁡x
30 25 29 sylib ⊢A∈No∧B∈No∧dom⁡A∈dom⁡B→¬∀x∈OnA⁡x=B⁡x