Step |
Hyp |
Ref |
Expression |
1 |
|
bnj907.1 |
⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) ) |
2 |
|
bnj907.2 |
⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
3 |
|
bnj907.3 |
⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) |
4 |
|
bnj907.4 |
⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
5 |
|
bnj907.5 |
⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) |
6 |
|
bnj907.6 |
⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) ) |
7 |
|
bnj907.7 |
⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 ) |
8 |
|
bnj907.8 |
⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 ) |
9 |
|
bnj907.9 |
⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 ) |
10 |
|
bnj907.10 |
⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ ) |
11 |
|
bnj907.11 |
⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ ) |
12 |
|
bnj907.12 |
⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ ) |
13 |
|
bnj907.13 |
⊢ 𝐷 = ( ω ∖ { ∅ } ) |
14 |
|
bnj907.14 |
⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } |
15 |
|
bnj907.15 |
⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 ) |
16 |
|
bnj907.16 |
⊢ 𝐺 = ( 𝑓 ∪ { 〈 𝑛 , 𝐶 〉 } ) |
17 |
1 2 3 4 5 6 13 14
|
bnj1021 |
⊢ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) |
18 |
|
vex |
⊢ 𝑝 ∈ V |
19 |
3 7 8 9 18
|
bnj919 |
⊢ ( 𝜒′ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′ ) ) |
20 |
16
|
bnj918 |
⊢ 𝐺 ∈ V |
21 |
19 10 11 12 20
|
bnj976 |
⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) ) |
22 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 21
|
bnj1020 |
⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
23 |
22
|
ax-gen |
⊢ ∀ 𝑚 ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
24 |
|
19.29r |
⊢ ( ( ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ∀ 𝑚 ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑚 ( ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) |
25 |
|
pm3.33 |
⊢ ( ( ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
26 |
24 25
|
bnj593 |
⊢ ( ( ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ∀ 𝑚 ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
27 |
23 26
|
mpan2 |
⊢ ( ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) → ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
28 |
27
|
2eximi |
⊢ ( ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) → ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
29 |
17 28
|
bnj101 |
⊢ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
30 |
|
19.9v |
⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
31 |
29 30
|
mpbi |
⊢ ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
32 |
|
19.9v |
⊢ ( ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
33 |
31 32
|
mpbi |
⊢ ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
34 |
|
19.9v |
⊢ ( ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
35 |
33 34
|
mpbi |
⊢ ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
36 |
|
19.9v |
⊢ ( ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) |
37 |
35 36
|
mpbi |
⊢ ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
38 |
4
|
bnj1254 |
⊢ ( 𝜃 → 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
39 |
37 38
|
sseldd |
⊢ ( 𝜃 → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) |
40 |
4 39
|
bnj978 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) ) |