Metamath Proof Explorer

Theorem indcardi

Description: Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015)

Ref Expression
Hypotheses indcardi.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
indcardi.b ⊢ ( 𝜑 → 𝑇 ∈ dom card )
indcardi.c ⊢ ( ( 𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀ 𝑦 ( 𝑆 ≺ 𝑅 → 𝜒 ) ) → 𝜓 )
indcardi.d ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
indcardi.e ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
indcardi.f ⊢ ( 𝑥 = 𝑦 → 𝑅 = 𝑆 )
indcardi.g ⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝑇 )
Assertion indcardi ( 𝜑 → 𝜃 )

Proof

Step Hyp Ref Expression
1 indcardi.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 indcardi.b ⊢ ( 𝜑 → 𝑇 ∈ dom card )
3 indcardi.c ⊢ ( ( 𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀ 𝑦 ( 𝑆 ≺ 𝑅 → 𝜒 ) ) → 𝜓 )
4 indcardi.d ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
5 indcardi.e ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
6 indcardi.f ⊢ ( 𝑥 = 𝑦 → 𝑅 = 𝑆 )
7 indcardi.g ⊢ ( 𝑥 = 𝐴 → 𝑅 = 𝑇 )
8 domrefg ⊢ ( 𝑇 ∈ dom card → 𝑇 ≼ 𝑇 )
9 2 8 syl ⊢ ( 𝜑 → 𝑇 ≼ 𝑇 )
10 cardon ⊢ ( card ‘ 𝑇 ) ∈ On
11 10 a1i ⊢ ( 𝜑 → ( card ‘ 𝑇 ) ∈ On )
12 simpl1 ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) ) ∧ 𝑅 ≼ 𝑇 ) → 𝜑 )
13 simpr ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) ) ∧ 𝑅 ≼ 𝑇 ) → 𝑅 ≼ 𝑇 )
14 simpr ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝑆 ≺ 𝑅 )
15 simpl1 ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝜑 )
16 15 2 syl ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝑇 ∈ dom card )
17 sdomdom ⊢ ( 𝑆 ≺ 𝑅 → 𝑆 ≼ 𝑅 )
18 simpl3 ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝑅 ≼ 𝑇 )
19 domtr ⊢ ( ( 𝑆 ≼ 𝑅 ∧ 𝑅 ≼ 𝑇 ) → 𝑆 ≼ 𝑇 )
20 17 18 19 syl2an2 ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝑆 ≼ 𝑇 )
21 numdom ⊢ ( ( 𝑇 ∈ dom card ∧ 𝑆 ≼ 𝑇 ) → 𝑆 ∈ dom card )
22 16 20 21 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝑆 ∈ dom card )
23 numdom ⊢ ( ( 𝑇 ∈ dom card ∧ 𝑅 ≼ 𝑇 ) → 𝑅 ∈ dom card )
24 16 18 23 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → 𝑅 ∈ dom card )
25 cardsdom2 ⊢ ( ( 𝑆 ∈ dom card ∧ 𝑅 ∈ dom card ) → ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) ↔ 𝑆 ≺ 𝑅 ) )
26 22 24 25 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) ↔ 𝑆 ≺ 𝑅 ) )
27 14 26 mpbird ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) )
28 id ⊢ ( ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) )
29 28 com3l ⊢ ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → ( ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → 𝜒 ) ) )
30 27 20 29 sylc ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) ∧ 𝑆 ≺ 𝑅 ) → ( ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → 𝜒 ) )
31 30 ex ⊢ ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) → ( 𝑆 ≺ 𝑅 → ( ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → 𝜒 ) ) )
32 31 com23 ⊢ ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) → ( ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → ( 𝑆 ≺ 𝑅 → 𝜒 ) ) )
33 32 alimdv ⊢ ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ 𝑅 ≼ 𝑇 ) → ( ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → ∀ 𝑦 ( 𝑆 ≺ 𝑅 → 𝜒 ) ) )
34 33 3exp ⊢ ( 𝜑 → ( ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) → ( 𝑅 ≼ 𝑇 → ( ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → ∀ 𝑦 ( 𝑆 ≺ 𝑅 → 𝜒 ) ) ) ) )
35 34 com34 ⊢ ( 𝜑 → ( ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) → ( ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) → ( 𝑅 ≼ 𝑇 → ∀ 𝑦 ( 𝑆 ≺ 𝑅 → 𝜒 ) ) ) ) )
36 35 3imp1 ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) ) ∧ 𝑅 ≼ 𝑇 ) → ∀ 𝑦 ( 𝑆 ≺ 𝑅 → 𝜒 ) )
37 12 13 36 3 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) ) ∧ 𝑅 ≼ 𝑇 ) → 𝜓 )
38 37 ex ⊢ ( ( 𝜑 ∧ ( ( card ‘ 𝑅 ) ∈ On ∧ ( card ‘ 𝑅 ) ⊆ ( card ‘ 𝑇 ) ) ∧ ∀ 𝑦 ( ( card ‘ 𝑆 ) ∈ ( card ‘ 𝑅 ) → ( 𝑆 ≼ 𝑇 → 𝜒 ) ) ) → ( 𝑅 ≼ 𝑇 → 𝜓 ) )
39 6 breq1d ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ≼ 𝑇 ↔ 𝑆 ≼ 𝑇 ) )
40 39 4 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ≼ 𝑇 → 𝜓 ) ↔ ( 𝑆 ≼ 𝑇 → 𝜒 ) ) )
41 7 breq1d ⊢ ( 𝑥 = 𝐴 → ( 𝑅 ≼ 𝑇 ↔ 𝑇 ≼ 𝑇 ) )
42 41 5 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑅 ≼ 𝑇 → 𝜓 ) ↔ ( 𝑇 ≼ 𝑇 → 𝜃 ) ) )
43 6 fveq2d ⊢ ( 𝑥 = 𝑦 → ( card ‘ 𝑅 ) = ( card ‘ 𝑆 ) )
44 7 fveq2d ⊢ ( 𝑥 = 𝐴 → ( card ‘ 𝑅 ) = ( card ‘ 𝑇 ) )
45 1 11 38 40 42 43 44 tfisi ⊢ ( 𝜑 → ( 𝑇 ≼ 𝑇 → 𝜃 ) )
46 9 45 mpd ⊢ ( 𝜑 → 𝜃 )