Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sltsgn1 Structured version   Visualization version   GIF version

Theorem sltsgn1 31512
 Description: If 𝐴
Assertion
Ref Expression
sltsgn1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜)))
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘

Proof of Theorem sltsgn1
StepHypRef Expression
1 sltval2 31507 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)})))
2 fvex 6158 . . . 4 (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) ∈ V
3 fvex 6158 . . . 4 (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) ∈ V
42, 3brtp 31344 . . 3 ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) ↔ (((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅) ∨ ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 2𝑜) ∨ ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 2𝑜)))
5 olc 399 . . . . 5 ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
65adantr 481 . . . 4 (((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅) → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
75adantr 481 . . . 4 (((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 2𝑜) → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
8 orc 400 . . . . 5 ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
98adantr 481 . . . 4 (((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 2𝑜) → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
106, 7, 93jaoi 1388 . . 3 ((((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅) ∨ ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜 ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 2𝑜) ∨ ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∧ (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 2𝑜)) → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
114, 10sylbi 207 . 2 ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜))
121, 11syl6bi 243 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 → ((𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = ∅ ∨ (𝐴 {𝑘 ∈ On ∣ (𝐴𝑘) ≠ (𝐵𝑘)}) = 1𝑜)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   ∨ w3o 1035   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  {crab 2911  ∅c0 3891  {ctp 4152  ⟨cop 4154  ∩ cint 4440   class class class wbr 4613  Oncon0 5682  ‘cfv 5847  1𝑜c1o 7498  2𝑜c2o 7499   No csur 31491
 Copyright terms: Public domain W3C validator