New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  lenltfin GIF version

Theorem lenltfin 4469
 Description: Less than or equal is the same as negated less than. (Contributed by SF, 2-Feb-2015.)
Assertion
Ref Expression
lenltfin ((A Nn B Nn ) → (⟪A, Bfin ↔ ¬ ⟪B, A <fin ))

Proof of Theorem lenltfin
StepHypRef Expression
1 ltfinirr 4457 . . . . . 6 (A Nn → ¬ ⟪A, A <fin )
21adantr 451 . . . . 5 ((A Nn B Nn ) → ¬ ⟪A, A <fin )
32adantr 451 . . . 4 (((A Nn B Nn ) A, Bfin ) → ¬ ⟪A, A <fin )
4 leltfintr 4458 . . . . . 6 ((A Nn B Nn A Nn ) → ((⟪A, Bfin B, A <fin ) → ⟪A, A <fin ))
543anidm13 1240 . . . . 5 ((A Nn B Nn ) → ((⟪A, Bfin B, A <fin ) → ⟪A, A <fin ))
65expdimp 426 . . . 4 (((A Nn B Nn ) A, Bfin ) → (⟪B, A <fin → ⟪A, A <fin ))
73, 6mtod 168 . . 3 (((A Nn B Nn ) A, Bfin ) → ¬ ⟪B, A <fin )
87ex 423 . 2 ((A Nn B Nn ) → (⟪A, Bfin → ¬ ⟪B, A <fin ))
9 nulge 4456 . . . . . 6 (( Nn A Nn ) → ⟪A, fin )
109ancoms 439 . . . . 5 ((A Nn Nn ) → ⟪A, fin )
11 eleq1 2413 . . . . . . 7 (B = → (B Nn Nn ))
1211anbi2d 684 . . . . . 6 (B = → ((A Nn B Nn ) ↔ (A Nn Nn )))
13 opkeq2 4060 . . . . . . 7 (B = → ⟪A, B⟫ = ⟪A, ⟫)
1413eleq1d 2419 . . . . . 6 (B = → (⟪A, Bfin ↔ ⟪A, fin ))
1512, 14imbi12d 311 . . . . 5 (B = → (((A Nn B Nn ) → ⟪A, Bfin ) ↔ ((A Nn Nn ) → ⟪A, fin )))
1610, 15mpbiri 224 . . . 4 (B = → ((A Nn B Nn ) → ⟪A, Bfin ))
1716a1dd 42 . . 3 (B = → ((A Nn B Nn ) → (¬ ⟪B, A <fin → ⟪A, Bfin )))
18 simplr 731 . . . . . . . 8 (((A Nn B Nn ) B) → B Nn )
19 simpll 730 . . . . . . . 8 (((A Nn B Nn ) B) → A Nn )
20 simpr 447 . . . . . . . 8 (((A Nn B Nn ) B) → B)
21 ltfintri 4466 . . . . . . . 8 ((B Nn A Nn B) → (⟪B, A <fin B = A A, B <fin ))
2218, 19, 20, 21syl3anc 1182 . . . . . . 7 (((A Nn B Nn ) B) → (⟪B, A <fin B = A A, B <fin ))
23 3orass 937 . . . . . . 7 ((⟪B, A <fin B = A A, B <fin ) ↔ (⟪B, A <fin (B = A A, B <fin )))
2422, 23sylib 188 . . . . . 6 (((A Nn B Nn ) B) → (⟪B, A <fin (B = A A, B <fin )))
2524ord 366 . . . . 5 (((A Nn B Nn ) B) → (¬ ⟪B, A <fin → (B = A A, B <fin )))
26 lefinrflx 4467 . . . . . . . . 9 (A Nn → ⟪A, Afin )
2726adantr 451 . . . . . . . 8 ((A Nn B Nn ) → ⟪A, Afin )
28 opkeq2 4060 . . . . . . . . 9 (B = A → ⟪A, B⟫ = ⟪A, A⟫)
2928eleq1d 2419 . . . . . . . 8 (B = A → (⟪A, Bfin ↔ ⟪A, Afin ))
3027, 29syl5ibrcom 213 . . . . . . 7 ((A Nn B Nn ) → (B = A → ⟪A, Bfin ))
3130adantr 451 . . . . . 6 (((A Nn B Nn ) B) → (B = A → ⟪A, Bfin ))
32 ltlefin 4468 . . . . . . 7 ((A Nn B Nn ) → (⟪A, B <fin → ⟪A, Bfin ))
3332adantr 451 . . . . . 6 (((A Nn B Nn ) B) → (⟪A, B <fin → ⟪A, Bfin ))
3431, 33jaod 369 . . . . 5 (((A Nn B Nn ) B) → ((B = A A, B <fin ) → ⟪A, Bfin ))
3525, 34syld 40 . . . 4 (((A Nn B Nn ) B) → (¬ ⟪B, A <fin → ⟪A, Bfin ))
3635expcom 424 . . 3 (B → ((A Nn B Nn ) → (¬ ⟪B, A <fin → ⟪A, Bfin )))
3717, 36pm2.61ine 2592 . 2 ((A Nn B Nn ) → (¬ ⟪B, A <fin → ⟪A, Bfin ))
388, 37impbid 183 1 ((A Nn B Nn ) → (⟪A, Bfin ↔ ¬ ⟪B, A <fin ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  ∅c0 3550  ⟪copk 4057   Nn cnnc 4373   ≤fin clefin 4432
 Copyright terms: Public domain W3C validator