Step |
Hyp |
Ref |
Expression |
1 |
|
ntrnei.o |
⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) ) |
2 |
|
ntrnei.f |
⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 ) |
3 |
|
ntrnei.r |
⊢ ( 𝜑 → 𝐼 𝐹 𝑁 ) |
4 |
1 2 3
|
ntrneif1o |
⊢ ( 𝜑 → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) |
5 |
1 2 3
|
ntrneinex |
⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) |
6 |
|
dff1o3 |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ↔ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ Fun ◡ 𝐹 ) ) |
7 |
6
|
simprbi |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → Fun ◡ 𝐹 ) |
8 |
7
|
adantr |
⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) → Fun ◡ 𝐹 ) |
9 |
|
df-rn |
⊢ ran 𝐹 = dom ◡ 𝐹 |
10 |
|
f1ofo |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) |
11 |
|
forn |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → ran 𝐹 = ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) |
12 |
10 11
|
syl |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → ran 𝐹 = ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) |
13 |
9 12
|
eqtr3id |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → dom ◡ 𝐹 = ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) |
14 |
13
|
eleq2d |
⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → ( 𝑁 ∈ dom ◡ 𝐹 ↔ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) ) |
15 |
14
|
biimpar |
⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) → 𝑁 ∈ dom ◡ 𝐹 ) |
16 |
8 15
|
jca |
⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) → ( Fun ◡ 𝐹 ∧ 𝑁 ∈ dom ◡ 𝐹 ) ) |
17 |
4 5 16
|
syl2anc |
⊢ ( 𝜑 → ( Fun ◡ 𝐹 ∧ 𝑁 ∈ dom ◡ 𝐹 ) ) |
18 |
|
funbrfvb |
⊢ ( ( Fun ◡ 𝐹 ∧ 𝑁 ∈ dom ◡ 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ↔ 𝑁 ◡ 𝐹 𝐼 ) ) |
19 |
17 18
|
syl |
⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ↔ 𝑁 ◡ 𝐹 𝐼 ) ) |
20 |
1 2 3
|
ntrneiiex |
⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) |
21 |
|
brcnvg |
⊢ ( ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝑁 ◡ 𝐹 𝐼 ↔ 𝐼 𝐹 𝑁 ) ) |
22 |
5 20 21
|
syl2anc |
⊢ ( 𝜑 → ( 𝑁 ◡ 𝐹 𝐼 ↔ 𝐼 𝐹 𝑁 ) ) |
23 |
19 22
|
bitrd |
⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ↔ 𝐼 𝐹 𝑁 ) ) |
24 |
3 23
|
mpbird |
⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ) |