Metamath Proof Explorer

Theorem wfi

Description: The Principle of Well-Ordered Induction. Theorem 6.27 of TakeutiZaring p. 32. This principle states that if B is a subclass of a well-ordered class A with the property that every element of B whose inital segment is included in A is itself equal to A . (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion wfi ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) ) ) → 𝐴 = 𝐵 )

Proof

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