Metamath Proof Explorer

Theorem constrfiss

Description: For any finite set A of constructible numbers, there is a n -th step ( Cn ) containing all numbers in A . (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrfiss.1 ⊢ ( 𝜑 → 𝐴 ⊆ Constr )
constrfiss.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion constrfiss ( 𝜑 → ∃ 𝑛 ∈ ω 𝐴 ⊆ ( 𝐶 ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrfiss.1 ⊢ ( 𝜑 → 𝐴 ⊆ Constr )
3 constrfiss.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
4 sseq1 ⊢ ( 𝑏 = ∅ → ( 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∅ ⊆ ( 𝐶 ‘ 𝑛 ) ) )
5 4 rexbidv ⊢ ( 𝑏 = ∅ → ( ∃ 𝑛 ∈ ω 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ω ∅ ⊆ ( 𝐶 ‘ 𝑛 ) ) )
6 sseq1 ⊢ ( 𝑏 = 𝑖 → ( 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) )
7 6 rexbidv ⊢ ( 𝑏 = 𝑖 → ( ∃ 𝑛 ∈ ω 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ω 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) )
8 sseq1 ⊢ ( 𝑏 = ( 𝑖 ∪ { 𝑥 } ) → ( 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
9 8 rexbidv ⊢ ( 𝑏 = ( 𝑖 ∪ { 𝑥 } ) → ( ∃ 𝑛 ∈ ω 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
10 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 𝑚 ) )
11 10 sseq2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ) )
12 11 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
13 9 12 bitrdi ⊢ ( 𝑏 = ( 𝑖 ∪ { 𝑥 } ) → ( ∃ 𝑛 ∈ ω 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ) )
14 sseq1 ⊢ ( 𝑏 = 𝐴 → ( 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ 𝐴 ⊆ ( 𝐶 ‘ 𝑛 ) ) )
15 14 rexbidv ⊢ ( 𝑏 = 𝐴 → ( ∃ 𝑛 ∈ ω 𝑏 ⊆ ( 𝐶 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ω 𝐴 ⊆ ( 𝐶 ‘ 𝑛 ) ) )
16 peano1 ⊢ ∅ ∈ ω
17 16 ne0ii ⊢ ω ≠ ∅
18 0ss ⊢ ∅ ⊆ ( 𝐶 ‘ 𝑛 )
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ω ) → ∅ ⊆ ( 𝐶 ‘ 𝑛 ) )
20 19 reximdva0 ⊢ ( ( 𝜑 ∧ ω ≠ ∅ ) → ∃ 𝑛 ∈ ω ∅ ⊆ ( 𝐶 ‘ 𝑛 ) )
21 17 20 mpan2 ⊢ ( 𝜑 → ∃ 𝑛 ∈ ω ∅ ⊆ ( 𝐶 ‘ 𝑛 ) )
22 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → 𝑙 ∈ ω )
23 fveq2 ⊢ ( 𝑚 = 𝑙 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑙 ) )
24 23 sseq2d ⊢ ( 𝑚 = 𝑙 → ( ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑙 ) ) )
25 24 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) ∧ 𝑚 = 𝑙 ) → ( ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑙 ) ) )
26 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) )
27 nnon ⊢ ( 𝑙 ∈ ω → 𝑙 ∈ On )
28 27 adantr ⊢ ( ( 𝑙 ∈ ω ∧ 𝑛 ∈ 𝑙 ) → 𝑙 ∈ On )
29 simpr ⊢ ( ( 𝑙 ∈ ω ∧ 𝑛 ∈ 𝑙 ) → 𝑛 ∈ 𝑙 )
30 1 28 29 constrmon ⊢ ( ( 𝑙 ∈ ω ∧ 𝑛 ∈ 𝑙 ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( 𝐶 ‘ 𝑙 ) )
31 22 30 sylancom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( 𝐶 ‘ 𝑙 ) )
32 26 31 sstrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → 𝑖 ⊆ ( 𝐶 ‘ 𝑙 ) )
33 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) )
34 33 snssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → { 𝑥 } ⊆ ( 𝐶 ‘ 𝑙 ) )
35 32 34 unssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑙 ) )
36 22 25 35 rspcedvd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 ∈ 𝑙 ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
37 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → 𝑛 ∈ ω )
38 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑛 ) )
39 38 sseq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
40 39 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) ∧ 𝑚 = 𝑛 ) → ( ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
41 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) )
42 nnon ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
43 42 adantr ⊢ ( ( 𝑛 ∈ ω ∧ 𝑙 ∈ 𝑛 ) → 𝑛 ∈ On )
44 simpr ⊢ ( ( 𝑛 ∈ ω ∧ 𝑙 ∈ 𝑛 ) → 𝑙 ∈ 𝑛 )
45 1 43 44 constrmon ⊢ ( ( 𝑛 ∈ ω ∧ 𝑙 ∈ 𝑛 ) → ( 𝐶 ‘ 𝑙 ) ⊆ ( 𝐶 ‘ 𝑛 ) )
46 37 45 sylancom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → ( 𝐶 ‘ 𝑙 ) ⊆ ( 𝐶 ‘ 𝑛 ) )
47 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) )
48 46 47 sseldd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑛 ) )
49 48 snssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → { 𝑥 } ⊆ ( 𝐶 ‘ 𝑛 ) )
50 41 49 unssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) )
51 37 40 50 rspcedvd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑛 ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
52 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → 𝑛 ∈ ω )
53 39 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) ∧ 𝑚 = 𝑛 ) → ( ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ↔ ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) ) )
54 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) )
55 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) )
56 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → 𝑛 = 𝑙 )
57 56 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → ( 𝐶 ‘ 𝑛 ) = ( 𝐶 ‘ 𝑙 ) )
58 55 57 eleqtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑛 ) )
59 58 snssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → { 𝑥 } ⊆ ( 𝐶 ‘ 𝑛 ) )
60 54 59 unssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑛 ) )
61 52 53 60 rspcedvd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) ∧ 𝑛 = 𝑙 ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
62 42 ad4antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) → 𝑛 ∈ On )
63 27 ad2antlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) → 𝑙 ∈ On )
64 oneltri ⊢ ( ( 𝑛 ∈ On ∧ 𝑙 ∈ On ) → ( 𝑛 ∈ 𝑙 ∨ 𝑙 ∈ 𝑛 ∨ 𝑛 = 𝑙 ) )
65 62 63 64 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) → ( 𝑛 ∈ 𝑙 ∨ 𝑙 ∈ 𝑛 ∨ 𝑛 = 𝑙 ) )
66 36 51 61 65 mpjao3dan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) ∧ 𝑙 ∈ ω ) ∧ 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
67 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝐴 ⊆ Constr )
68 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) )
69 68 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑥 ∈ 𝐴 )
70 67 69 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → 𝑥 ∈ Constr )
71 1 isconstr ⊢ ( 𝑥 ∈ Constr ↔ ∃ 𝑙 ∈ ω 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) )
72 70 71 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑙 ∈ ω 𝑥 ∈ ( 𝐶 ‘ 𝑙 ) )
73 66 72 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ 𝑛 ∈ ω ) ∧ 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
74 73 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ∧ ∃ 𝑛 ∈ ω 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) )
75 74 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) → ( ∃ 𝑛 ∈ ω 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ) )
76 75 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ⊆ 𝐴 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑖 ) ) ) → ( ∃ 𝑛 ∈ ω 𝑖 ⊆ ( 𝐶 ‘ 𝑛 ) → ∃ 𝑚 ∈ ω ( 𝑖 ∪ { 𝑥 } ) ⊆ ( 𝐶 ‘ 𝑚 ) ) )
77 5 7 13 15 21 76 3 findcard2d ⊢ ( 𝜑 → ∃ 𝑛 ∈ ω 𝐴 ⊆ ( 𝐶 ‘ 𝑛 ) )