Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
⊢ ( 𝑔 = 𝑘 → ( 𝑔 𝑞 𝑛 ↔ 𝑘 𝑞 𝑛 ) ) |
2 |
1
|
notbid |
⊢ ( 𝑔 = 𝑘 → ( ¬ 𝑔 𝑞 𝑛 ↔ ¬ 𝑘 𝑞 𝑛 ) ) |
3 |
2
|
cbvralvw |
⊢ ( ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ↔ ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑛 ) |
4 |
|
breq2 |
⊢ ( 𝑛 = 𝑚 → ( 𝑘 𝑞 𝑛 ↔ 𝑘 𝑞 𝑚 ) ) |
5 |
4
|
notbid |
⊢ ( 𝑛 = 𝑚 → ( ¬ 𝑘 𝑞 𝑛 ↔ ¬ 𝑘 𝑞 𝑚 ) ) |
6 |
5
|
ralbidv |
⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑛 ↔ ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) |
7 |
3 6
|
syl5bb |
⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ↔ ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) |
8 |
7
|
cbvriotavw |
⊢ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) = ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) |
9 |
|
rneq |
⊢ ( ℎ = 𝑑 → ran ℎ = ran 𝑑 ) |
10 |
9
|
raleqdv |
⊢ ( ℎ = 𝑑 → ( ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 ↔ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 ) ) |
11 |
10
|
rabbidv |
⊢ ( ℎ = 𝑑 → { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } = { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ) |
12 |
11
|
raleqdv |
⊢ ( ℎ = 𝑑 → ( ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ↔ ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) |
13 |
11 12
|
riotaeqbidv |
⊢ ( ℎ = 𝑑 → ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) = ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) |
14 |
8 13
|
eqtrid |
⊢ ( ℎ = 𝑑 → ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) = ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) |
15 |
14
|
cbvmptv |
⊢ ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) = ( 𝑑 ∈ V ↦ ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) |
16 |
|
recseq |
⊢ ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) = ( 𝑑 ∈ V ↦ ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) → recs ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) = recs ( ( 𝑑 ∈ V ↦ ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) ) ) |
17 |
15 16
|
ax-mp |
⊢ recs ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) = recs ( ( 𝑑 ∈ V ↦ ( ℩ 𝑚 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ∀ 𝑘 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } ¬ 𝑘 𝑞 𝑚 ) ) ) |
18 |
|
breq1 |
⊢ ( 𝑞 = 𝑠 → ( 𝑞 𝑅 𝑣 ↔ 𝑠 𝑅 𝑣 ) ) |
19 |
18
|
cbvralvw |
⊢ ( ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 ↔ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑣 ) |
20 |
|
breq2 |
⊢ ( 𝑣 = 𝑟 → ( 𝑠 𝑅 𝑣 ↔ 𝑠 𝑅 𝑟 ) ) |
21 |
20
|
ralbidv |
⊢ ( 𝑣 = 𝑟 → ( ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑣 ↔ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑟 ) ) |
22 |
19 21
|
syl5bb |
⊢ ( 𝑣 = 𝑟 → ( ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 ↔ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑟 ) ) |
23 |
22
|
cbvrabv |
⊢ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran 𝑑 𝑞 𝑅 𝑣 } = { 𝑟 ∈ 𝐴 ∣ ∀ 𝑠 ∈ ran 𝑑 𝑠 𝑅 𝑟 } |
24 |
|
eqid |
⊢ { 𝑟 ∈ 𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑢 ) 𝑠 𝑅 𝑟 } = { 𝑟 ∈ 𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑢 ) 𝑠 𝑅 𝑟 } |
25 |
|
eqid |
⊢ { 𝑟 ∈ 𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑡 ) 𝑠 𝑅 𝑟 } = { 𝑟 ∈ 𝐴 ∣ ∀ 𝑠 ∈ ( recs ( ( ℎ ∈ V ↦ ( ℩ 𝑛 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ∀ 𝑔 ∈ { 𝑣 ∈ 𝐴 ∣ ∀ 𝑞 ∈ ran ℎ 𝑞 𝑅 𝑣 } ¬ 𝑔 𝑞 𝑛 ) ) ) “ 𝑡 ) 𝑠 𝑅 𝑟 } |
26 |
17 23 24 25
|
zorn2lem7 |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀ 𝑤 ( ( 𝑤 ⊆ 𝐴 ∧ 𝑅 Or 𝑤 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝑤 ( 𝑧 𝑅 𝑥 ∨ 𝑧 = 𝑥 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) |