Metamath Proof Explorer

Theorem frind

Description: The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin ). This principle states that if B is a subclass of a founded class A with the property that every element of B whose initial segment is included in A is itself equal to A . Compare wfi and tfi , which are special cases of this theorem that do not require the axiom of infinity to prove. (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 ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) → 𝐴 = 𝐵 )