Metamath Proof Explorer


Theorem frind

Description: A subclass of a well-founded class A with the property that whenever it contains all predecessors of an element of A it also contains that element, is equal to A . Compare wfi and tfi , which are special cases of this theorem that do not require the axiom of infinity. (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion frind ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴 ∧ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 ssdif0 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = ∅ )
2 1 necon3bbii ( ¬ 𝐴𝐵 ↔ ( 𝐴𝐵 ) ≠ ∅ )
3 difss ( 𝐴𝐵 ) ⊆ 𝐴
4 frmin ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ( ( 𝐴𝐵 ) ⊆ 𝐴 ∧ ( 𝐴𝐵 ) ≠ ∅ ) ) → ∃ 𝑦 ∈ ( 𝐴𝐵 ) Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ )
5 eldif ( 𝑦 ∈ ( 𝐴𝐵 ) ↔ ( 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) )
6 5 anbi1i ( ( 𝑦 ∈ ( 𝐴𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ↔ ( ( 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) )
7 anass ( ( ( 𝑦𝐴 ∧ ¬ 𝑦𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ↔ ( 𝑦𝐴 ∧ ( ¬ 𝑦𝐵 ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ) )
8 ancom ( ( ¬ 𝑦𝐵 ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ↔ ( Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ∧ ¬ 𝑦𝐵 ) )
9 indif2 ( ( 𝑅 “ { 𝑦 } ) ∩ ( 𝐴𝐵 ) ) = ( ( ( 𝑅 “ { 𝑦 } ) ∩ 𝐴 ) ∖ 𝐵 )
10 df-pred Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ( ( 𝐴𝐵 ) ∩ ( 𝑅 “ { 𝑦 } ) )
11 incom ( ( 𝐴𝐵 ) ∩ ( 𝑅 “ { 𝑦 } ) ) = ( ( 𝑅 “ { 𝑦 } ) ∩ ( 𝐴𝐵 ) )
12 10 11 eqtri Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ( ( 𝑅 “ { 𝑦 } ) ∩ ( 𝐴𝐵 ) )
13 df-pred Pred ( 𝑅 , 𝐴 , 𝑦 ) = ( 𝐴 ∩ ( 𝑅 “ { 𝑦 } ) )
14 incom ( 𝐴 ∩ ( 𝑅 “ { 𝑦 } ) ) = ( ( 𝑅 “ { 𝑦 } ) ∩ 𝐴 )
15 13 14 eqtri Pred ( 𝑅 , 𝐴 , 𝑦 ) = ( ( 𝑅 “ { 𝑦 } ) ∩ 𝐴 )
16 15 difeq1i ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) = ( ( ( 𝑅 “ { 𝑦 } ) ∩ 𝐴 ) ∖ 𝐵 )
17 9 12 16 3eqtr4i Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 )
18 17 eqeq1i ( Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) = ∅ )
19 ssdif0 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∖ 𝐵 ) = ∅ )
20 18 19 bitr4i ( Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ↔ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
21 20 anbi1i ( ( Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ∧ ¬ 𝑦𝐵 ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦𝐵 ) )
22 8 21 bitri ( ( ¬ 𝑦𝐵 ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ↔ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦𝐵 ) )
23 22 anbi2i ( ( 𝑦𝐴 ∧ ( ¬ 𝑦𝐵 ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ) ↔ ( 𝑦𝐴 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦𝐵 ) ) )
24 6 7 23 3bitri ( ( 𝑦 ∈ ( 𝐴𝐵 ) ∧ Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ) ↔ ( 𝑦𝐴 ∧ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦𝐵 ) ) )
25 24 rexbii2 ( ∃ 𝑦 ∈ ( 𝐴𝐵 ) Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ↔ ∃ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦𝐵 ) )
26 rexanali ( ∃ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ ¬ 𝑦𝐵 ) ↔ ¬ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) )
27 25 26 bitri ( ∃ 𝑦 ∈ ( 𝐴𝐵 ) Pred ( 𝑅 , ( 𝐴𝐵 ) , 𝑦 ) = ∅ ↔ ¬ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) )
28 4 27 sylib ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ( ( 𝐴𝐵 ) ⊆ 𝐴 ∧ ( 𝐴𝐵 ) ≠ ∅ ) ) → ¬ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) )
29 28 ex ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) → ( ( ( 𝐴𝐵 ) ⊆ 𝐴 ∧ ( 𝐴𝐵 ) ≠ ∅ ) → ¬ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) )
30 3 29 mpani ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) → ( ( 𝐴𝐵 ) ≠ ∅ → ¬ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) )
31 2 30 syl5bi ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) → ( ¬ 𝐴𝐵 → ¬ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) )
32 31 con4d ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) → ( ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) → 𝐴𝐵 ) )
33 32 imp ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) → 𝐴𝐵 )
34 33 adantrl ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴 ∧ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) ) → 𝐴𝐵 )
35 simprl ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴 ∧ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) ) → 𝐵𝐴 )
36 34 35 eqssd ( ( ( 𝑅 Fr 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐵𝐴 ∧ ∀ 𝑦𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵𝑦𝐵 ) ) ) → 𝐴 = 𝐵 )